let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
let p be Element of CQC-WFF A; :: thesis: for x, y being bound_QC-variable of A holds
( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
let x, y be bound_QC-variable of A; :: thesis: ( (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid & (All (x,y,p)) => (All (y,x,p)) is valid )
not y in still_not-bound_in (All (y,p)) by Th5;
then A1: not y in still_not-bound_in (All (x,(All (y,p)))) by Th5;
( All (x,((All (y,p)) => p)) is valid & (All (x,((All (y,p)) => p))) => ((All (x,(All (y,p)))) => (All (x,p))) is valid ) by Th23, Th30, CQC_THE1:66;
then (All (x,(All (y,p)))) => (All (x,p)) is valid by CQC_THE1:65;
hence (All (x,(All (y,p)))) => (All (y,(All (x,p)))) is valid by A1, CQC_THE1:67; :: thesis: (All (x,y,p)) => (All (y,x,p)) is valid
then (All (x,y,p)) => (All (y,(All (x,p)))) is valid by QC_LANG2:14;
hence (All (x,y,p)) => (All (y,x,p)) is valid by QC_LANG2:14; :: thesis: verum