:: deftheorem Def3 defines CQCSub_& SUBLEMMA:def 3 :
for Al being QC-alphabet
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
CQCSub_& (S1,S2) = Sub_& (S1,S2);