defpred S₁[ set ] means ex H1 being strict Subgroup of G st
( $1 = H1 & H,H1 are_conjugated );
consider L being Subset of (Subgroups G) such that
A1: for x being set holds
( x in L iff ( x in Subgroups G & S₁[x] ) ) from SUBSET_1:sch 1();
take L ; :: thesis: for x being object holds
( x in L iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
let x be object ; :: thesis: ( x in L iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) )
thus ( x in L implies ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) by A1; :: thesis: ( ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) implies x in L )
given H1 being strict Subgroup of G such that A2: x = H1 and
A3: H,H1 are_conjugated ; :: thesis: x in L
x in Subgroups G by A2, Def1;
hence x in L by A1, A2, A3; :: thesis: verum