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 )
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 Th26, Th34, CQC_THE1:105;
then (All x,(All y,p)) => (All x,p) is valid by CQC_THE1:104;
hence (All x,(All y,p)) => (All y,(All x,p)) is valid by A1, 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