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