defpred S_{1}[ 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_{1}[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_{1}[x] )
; :: thesis: A1 = A2

thus A1 = A2 from XBOOLE_0:sch 2(A11, A12); :: thesis: verum

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 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

thus A1 = A2 from XBOOLE_0:sch 2(A11, A12); :: thesis: verum