let p, r, q be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> holds
|- (f ^ <*(p 'or' q)*>) ^ <*r*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> implies |- (f ^ <*(p 'or' q)*>) ^ <*r*> )
set f1 = (f ^ <*('not' r)*>) ^ <*('not' p)*>;
set f2 = (f ^ <*('not' r)*>) ^ <*('not' q)*>;
A1: ( Suc ((f ^ <*('not' r)*>) ^ <*('not' p)*>) = 'not' p & Suc ((f ^ <*('not' r)*>) ^ <*('not' q)*>) = 'not' q ) by Th5;
assume ( |- (f ^ <*p*>) ^ <*r*> & |- (f ^ <*q*>) ^ <*r*> ) ; :: thesis: |- (f ^ <*(p 'or' q)*>) ^ <*r*>
then A2: ( |- (f ^ <*('not' r)*>) ^ <*('not' p)*> & |- (f ^ <*('not' r)*>) ^ <*('not' q)*> ) by Th46;
A3: Ant ((f ^ <*('not' r)*>) ^ <*('not' p)*>) = f ^ <*('not' r)*> by Th5;
then Ant ((f ^ <*('not' r)*>) ^ <*('not' p)*>) = Ant ((f ^ <*('not' r)*>) ^ <*('not' q)*>) by Th5;
then |- (f ^ <*('not' r)*>) ^ <*(('not' p) '&' ('not' q))*> by A2, A1, A3, Th39;
then |- (f ^ <*('not' (('not' p) '&' ('not' q)))*>) ^ <*r*> by Th48;
hence |- (f ^ <*(p 'or' q)*>) ^ <*r*> by QC_LANG2:def 3; :: thesis: verum