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