let S1, S2 be Element of CQC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 implies (CQCSub_& (S1,S2)) `2 = S1 `2 )
assume A1: S1 `2 = S2 `2 ; :: thesis: (CQCSub_& (S1,S2)) `2 = S1 `2
then CQCSub_& (S1,S2) = Sub_& (S1,S2) by Def4;
then CQCSub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, SUBSTUT1:def 21;
hence (CQCSub_& (S1,S2)) `2 = S1 `2 by MCART_1:7; :: thesis: verum