let p be Nat; :: thesis: for G being finite strict Group st card G = p & p is prime holds
for H being strict Subgroup of G holds
( H = (1). G or H = G )
let G be finite strict Group; :: thesis: ( card G = p & p is prime implies for H being strict Subgroup of G holds
( H = (1). G or H = G ) )
assume that
A1: card G = p and
A2: p is prime ; :: thesis: for H being strict Subgroup of G holds
( H = (1). G or H = G )
let H be strict Subgroup of G; :: thesis: ( H = (1). G or H = G )
card H divides p by A1, GROUP_2:148;
then ( card H = 1 or card H = p ) by A2, INT_2:def 4;
hence ( H = (1). G or H = G ) by A1, GROUP_2:70, GROUP_2:73; :: thesis: verum