let p, q be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable holds (Ex x,(p 'or' q)) <=> ((Ex x,p) 'or' (Ex x,q)) is valid
let x be bound_QC-variable; :: thesis: (Ex x,(p 'or' q)) <=> ((Ex x,p) 'or' (Ex x,q)) is valid
( (Ex x,(p 'or' q)) => ((Ex x,p) 'or' (Ex x,q)) is valid & ((Ex x,p) 'or' (Ex x,q)) => (Ex x,(p 'or' q)) is valid ) by Th44;
hence (Ex x,(p 'or' q)) <=> ((Ex x,p) 'or' (Ex x,q)) is valid by Lm14; :: thesis: verum