let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
let x be bound_QC-variable; :: thesis: (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid
All (x,((p '&' q) => q)) is valid by Lm1, Th26;
then A1: (Ex (x,(p '&' q))) => (Ex (x,q)) is valid by Th39;
All (x,((p '&' q) => p)) is valid by Lm1, Th26;
then (Ex (x,(p '&' q))) => (Ex (x,p)) is valid by Th39;
hence (Ex (x,(p '&' q))) => ((Ex (x,p)) '&' (Ex (x,q))) is valid by A1, Lm3; :: thesis: verum