let G be finite Group; :: thesis: for H being Subgroup of G st card H <> card G holds
ex a being Element of G st not a in H
let H be Subgroup of G; :: thesis: ( card H <> card G implies ex a being Element of G st not a in H )
assume A1: card H <> card G ; :: thesis: not for a being Element of G holds a in H
assume for a being Element of G holds a in H ; :: thesis: contradiction
then multMagma(# the carrier of H, the multF of H #) = multMagma(# the carrier of G, the multF of G #) by GROUP_2:62;
hence contradiction by A1; :: thesis: verum