theorem Th52: :: CALCUL_1:53

for Al being QC-alphabet
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*>