theorem Th23: :: SUBLEMMA:23

for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQC_Sub (CQCSub_& (S1,S2)) = (CQC_Sub S1) '&' (CQC_Sub S2)