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

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