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
( (p '&' q) => p is valid & (p '&' q) => q is valid ) by Lm1;
then ( All x,((p '&' q) => p) is valid & All x,((p '&' q) => q) is valid ) by Th26;
then ( (Ex x,(p '&' q)) => (Ex x,p) is valid & (Ex x,(p '&' q)) => (Ex x,q) is valid ) by Th39;
hence (Ex x,(p '&' q)) => ((Ex x,p) '&' (Ex x,q)) is valid by Lm3; :: thesis: verum