for x being set
for G being addGroup
for H being Subgroup of G st x in con_class H holds
x is strict Subgroup of G