defpred S₁[ object ] means ex H3 being strict Subgroup of G st
( $1 = H3 & H,H3 are_conjugated );
let A1, A2 be Subset of (Subgroups G); :: thesis: ( ( for x being object holds
( x in A1 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) & ( for x being object holds
( x in A2 iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) ) implies A1 = A2 )
assume A4: for x being object holds
( x in A1 iff S₁[x] ) ; :: thesis: ( ex x being object st
( ( x in A2 implies ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) implies ( ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) & not x in A2 ) ) or A1 = A2 )
assume A5: for x being object holds
( x in A2 iff S₁[x] ) ; :: thesis: A1 = A2
thus A1 = A2 from XBOOLE_0:sch 2(A4, A5); :: thesis: verum