for G being finite Group
for H being Subgroup of G st card H <> card G holds
ex a being Element of G st not a in H