let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable st not x in still_not-bound_in p holds
( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
let x be bound_QC-variable; :: thesis: ( not x in still_not-bound_in p implies ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid ) )
assume A1: not x in still_not-bound_in p ; :: thesis: ( (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid & (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid )
(p '&' q) => (Ex (x,(p '&' q))) is valid by Th18;
then A2: q => (p => (Ex (x,(p '&' q)))) is valid by Th4;
not x in still_not-bound_in (Ex (x,(p '&' q))) by Th6;
then not x in still_not-bound_in (p => (Ex (x,(p '&' q)))) by A1, Th7;
then (Ex (x,q)) => (p => (Ex (x,(p '&' q)))) is valid by A2, Th22;
hence (p '&' (Ex (x,q))) => (Ex (x,(p '&' q))) is valid by Th2; :: thesis: (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid
q => (Ex (x,q)) is valid by Th18;
then A3: (p '&' q) => (p '&' (Ex (x,q))) is valid by Lm9;
not x in still_not-bound_in (Ex (x,q)) by Th6;
then not x in still_not-bound_in (p '&' (Ex (x,q))) by A1, Th9;
hence (Ex (x,(p '&' q))) => (p '&' (Ex (x,q))) is valid by A3, Th22; :: thesis: verum