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