consider S1, S2 being Element of QC-Sub-WFF such that
A2: ( S = Sub_& (S1,S2) & S1 `2 = S2 `2 ) by A1, Def27;
take S2 ; :: thesis: ex S9 being Element of QC-Sub-WFF st
( S = Sub_& (S9,S2) & S9 `2 = S2 `2 )
thus ex S9 being Element of QC-Sub-WFF st
( S = Sub_& (S9,S2) & S9 `2 = S2 `2 ) by A2; :: thesis: verum