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