theorem Th5: :: GOEDELCP:5

for Al being QC-alphabet
for p, q being Element of CQC-WFF Al
for f1 being FinSequence of CQC-WFF Al st |- f1 ^ <*p*> & |- f1 ^ <*q*> holds
|- f1 ^ <*(p '&' q)*>