theorem Th20: :: SUBLEMMA:20

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