theorem Th22: :: CALCUL_2:22

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