let Al be QC-alphabet ; for S1, S2 being Element of CQC-Sub-WFF Al st S1 `2 = S2 `2 holds
(CQCSub_& (S1,S2)) `2 = S1 `2
let S1, S2 be Element of CQC-Sub-WFF Al; ( S1 `2 = S2 `2 implies (CQCSub_& (S1,S2)) `2 = S1 `2 )
assume A1:
S1 `2 = S2 `2
; (CQCSub_& (S1,S2)) `2 = S1 `2
then
CQCSub_& (S1,S2) = Sub_& (S1,S2)
by Def3;
then
CQCSub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)]
by A1, SUBSTUT1:def 21;
hence
(CQCSub_& (S1,S2)) `2 = S1 `2
; verum