let p be Element of 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:178;
then ( card H = 1 or card H = p ) by A2, INT_2:def 5;
hence ( H = (1). G or H = G ) by A1, GROUP_2:82, GROUP_2:85; :: thesis: verum