Sub_& (S1,S2) = [((S1 `1) '&' (S2 `1)),(S1 `2)] by A1, SUBSTUT1:def 21;
then (Sub_& (S1,S2)) `1 = (S1 `1) '&' (S2 `1) by MCART_1:7;
then Sub_& (S1,S2) in CQC-Sub-WFF by SUBSTUT1:def 39;
hence Sub_& (S1,S2) is Element of CQC-Sub-WFF ; :: thesis: verum