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