let G be finite Group; :: thesis: for H being strict Subgroup of G st index H = card G holds
H = (1). G
let H be strict Subgroup of G; :: thesis: ( index H = card G implies H = (1). G )
assume index H = card G ; :: thesis: H = (1). G
then 1 * (card G) = (card H) * (card G) by Th147;
hence H = (1). G by Th70, XCMPLX_1:5; :: thesis: verum