let p be Element of CQC-WFF ; :: thesis: for x, y being bound_QC-variable holds (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid
let x, y be bound_QC-variable; :: thesis: (Ex (x,(All (y,p)))) => (All (y,(Ex (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 (All (y,(Ex (x,p)))) by Th5;
( All (y,(p => (Ex (x,p)))) is valid & (All (y,(p => (Ex (x,p))))) => ((All (y,p)) => (All (y,(Ex (x,p))))) is valid ) by Th18, Th26, Th34;
then (All (y,p)) => (All (y,(Ex (x,p)))) is valid by CQC_THE1:65;
hence (Ex (x,(All (y,p)))) => (All (y,(Ex (x,p)))) is valid by A1, Th22; :: thesis: verum