let p, q be Element of CQC-WFF ; :: thesis: for h being QC-formula
for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All x,p <==> All y,q
let h be QC-formula; :: thesis: for x, y being bound_QC-variable st p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h holds
All x,p <==> All y,q
let x, y be bound_QC-variable; :: thesis: ( p = h . x & q = h . y & not x in still_not-bound_in h & not y in still_not-bound_in h implies All x,p <==> All y,q )
assume that
A1: p = h . x and
A2: q = h . y and
A3: not x in still_not-bound_in h and
A4: not y in still_not-bound_in h ; :: thesis: All x,p <==> All y,q

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: All x,p <==> All y,q

hence All x,p <==> All y,q by A1, A2; :: thesis: verum

end;

suppose A5: x <> y ; :: thesis: All x,p <==> All y,q

then A6: not y in still_not-bound_in p by A1, A4, Th65;
not x in still_not-bound_in q by A2, A3, A5, Th65;
then ( (All x,p) => (All y,q) is valid & (All y,q) => (All x,p) is valid ) by A1, A2, A3, A4, A6, CQC_THE2:30;
hence All x,p <==> All y,q by Th50; :: thesis: verum

end;

end;