for Al being QC-alphabet
for A being non empty set
for v being Element of Valuations_in (Al,A)
for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
( Val_S (v,S1) = Val_S (v,(CQCSub_& (S1,S2))) & Val_S (v,S2) = Val_S (v,(CQCSub_& (S1,S2))) ) by Th21;