let S1, S2 be Element of QC-Sub-WFF ; :: thesis: ( S1 `2 = S2 `2 implies Sub_& S1,S2 is Sub_conjunctive )
assume A1: S1 `2 = S2 `2 ; :: thesis: Sub_& S1,S2 is Sub_conjunctive
take S1 ; :: according to SUBSTUT1:def 27 :: thesis: ex S2 being Element of QC-Sub-WFF st
( Sub_& S1,S2 = Sub_& S1,S2 & S1 `2 = S2 `2 )
take S2 ; :: thesis: ( Sub_& S1,S2 = Sub_& S1,S2 & S1 `2 = S2 `2 )
thus ( Sub_& S1,S2 = Sub_& S1,S2 & S1 `2 = S2 `2 ) by A1; :: thesis: verum