let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable 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; :: thesis: ( (All x,(All y,p)) => (All y,(All x,p)) is valid & (All x,y,p) => (All y,x,p) is valid )
A1: All x,((All y,p) => p) is valid by Th26, CQC_THE1:105;
(All x,((All y,p) => p)) => ((All x,(All y,p)) => (All x,p)) is valid by Th34;
then A2: (All x,(All y,p)) => (All x,p) is valid by A1, CQC_THE1:104;
not y in still_not-bound_in (All y,p) by Th5;
then not y in still_not-bound_in (All x,(All y,p)) by Th5;
hence (All x,(All y,p)) => (All y,(All x,p)) is valid by A2, CQC_THE1:106; :: 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:20;
hence (All x,y,p) => (All y,x,p) is valid by QC_LANG2:20; :: thesis: verum