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