defpred S₁[ object ] means $1 is strict StableSubgroup of G;
let A1, A2 be set ; :: thesis: ( ( for x being object holds
( x in A1 iff x is strict StableSubgroup of G ) ) & ( for x being object holds
( x in A2 iff x is strict StableSubgroup of G ) ) implies A1 = A2 )
assume A11: for x being object holds
( x in A1 iff S₁[x] ) ; :: thesis: ( ex x being object st
( ( x in A2 implies x is strict StableSubgroup of G ) implies ( x is strict StableSubgroup of G & not x in A2 ) ) or A1 = A2 )
assume A12: for x being object holds
( x in A2 iff S₁[x] ) ; :: thesis: A1 = A2
thus A1 = A2 from XBOOLE_0:sch 2(A11, A12); :: thesis: verum