let p, q be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable st p |-| q holds
All x,p |-| All y,q
let x, y be bound_QC-variable; :: thesis: ( p |-| q implies All x,p |-| All y,q )
assume A1: p |-| q ; :: thesis: All x,p |-| All y,q
All x,p |-| p by Th36;
then A2: All x,p |-| q by A1, Th28;
q |-| All y,q by Th36;
hence All x,p |-| All y,q by A2, Th28; :: thesis: verum