let A be QC-alphabet ; :: thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_& (S1,S2) is Sub_conjunctive
let S1, S2 be Element of QC-Sub-WFF A; :: 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 A 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