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