let x be set ; :: thesis: for G being Group
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
let G be Group; :: thesis: for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G
let H be Subgroup of G; :: thesis: ( x in con_class H implies x is strict Subgroup of G )
assume x in con_class H ; :: thesis: x is strict Subgroup of G
then ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) by Def12;
hence x is strict Subgroup of G ; :: thesis: verum