let G be strict Group; :: thesis: ( ex a being Element of G st a <> 1_ G implies ( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) ) )
assume A1: ex a being Element of G st a <> 1_ G ; :: thesis: ( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) iff ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) )
thus ( ( for H being strict Subgroup of G holds
( H = G or H = (1). G ) ) implies ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) ) :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) implies for H being strict Subgroup of G holds
( H = G or H = (1). G ) )

proof

assume A2: for H being strict Subgroup of G holds
( H = G or H = (1). G ) ; :: thesis: ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) )
consider b being Element of G such that
A3: b <> 1_ G by A1;
A4: gr {b} = G by A2, A3, Th7;
A5: not b is being_of_order_0

proof

assume A6: b is being_of_order_0 ; :: thesis: contradiction
then A7: b |^ 2 <> 1_ G by GROUP_1:def 10;
not b in gr {(b |^ 2)}

proof

assume b in gr {(b |^ 2)} ; :: thesis: contradiction
then consider j1 being Integer such that
A8: b = (b |^ 2) |^ j1 by GR_CY_1:5;
b = b |^ (2 * j1) by A8, GROUP_1:35;
then (b ") * (b |^ (2 * j1)) = 1_ G by GROUP_1:def 5;
then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:32;
then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:33;
then (- 1) + (2 * j1) = 0 by A6, Th13;
hence contradiction by INT_1:9; :: thesis: verum

end;

then gr {(b |^ 2)} <> G ;
hence contradiction by A2, A7, Th7; :: thesis: verum

end;

then consider n being Element of NAT such that
A9: n = ord b and
not b is being_of_order_0 ;
A10: G is finite by A4, A5, Th11;
then A11: card G = n by A4, A9, GR_CY_1:7;
n is prime

proof

assume A12: not n is prime ; :: thesis: contradiction
ex u, v being Element of NAT st
( u > 1 & v > 1 & n = u * v )

proof

A13: ( not n > 1 or ex m being Nat st
( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def 4;
n >= 1 by A10, A11, GROUP_1:45;
then n > 1 by A3, A9, GROUP_1:43, XXREAL_0:1;
then consider m being Nat such that
A14: m <> 1 and
A15: m <> n and
A16: m divides n by A13;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
consider o being Nat such that
A17: n = m * o by A16, NAT_D:def 3;
reconsider o = o as Element of NAT by ORDINAL1:def 12;
take u = m; :: thesis: ex v being Element of NAT st
( u > 1 & v > 1 & n = u * v )
take v = o; :: thesis: ( u > 1 & v > 1 & n = u * v )
u <> 0

proof

assume u = 0 ; :: thesis: contradiction
then n = 0 * (n div 0) by A16, NAT_D:3;
hence contradiction by A10, A11; :: thesis: verum

end;

then A18: 0 + 1 <= u by INT_1:7;
0 < v by A10, A11, A17;
then A19: 0 + 1 <= v by INT_1:7;
v <> 1 by A15, A17;
hence ( u > 1 & v > 1 & n = u * v ) by A14, A17, A18, A19, XXREAL_0:1; :: thesis: verum

end;

then consider u, v being Element of NAT such that
A20: u > 1 and
A21: v > 1 and
A22: n = u * v ;
ord (b |^ v) = u by A4, A10, A11, A22, GR_CY_2:8;
then A23: card (gr {(b |^ v)}) = u by A10, GR_CY_1:7;
A24: u <> n by A20, A21, A22, XCMPLX_1:7;
gr {(b |^ v)} <> (1). G by A20, A23, GROUP_2:69;
hence contradiction by A2, A11, A23, A24; :: thesis: verum

end;

hence ( G is cyclic & G is finite & ex p being Element of NAT st
( card G = p & p is prime ) ) by A4, A5, A11, Th11, GR_CY_2:4; :: thesis: verum

end;

assume that
G is cyclic and
A25: G is finite and
A26: ex p being Element of NAT st
( card G = p & p is prime ) ; :: thesis: for H being strict Subgroup of G holds
( H = G or H = (1). G )
let H be strict Subgroup of G; :: thesis: ( H = G or H = (1). G )
reconsider G = G as finite Group by A25;
reconsider H = H as Subgroup of G ;
card G = (card H) * (index H) by GROUP_2:147;
then A27: card H divides card G by NAT_D:def 3;

per cases ( card H = card G or card H = 1 ) by A26, A27, INT_2:def 4;

suppose card H = card G ; :: thesis: ( H = G or H = (1). G )

hence ( H = G or H = (1). G ) by GROUP_2:73; :: thesis: verum

end;

suppose card H = 1 ; :: thesis: ( H = G or H = (1). G )

hence ( H = G or H = (1). G ) by GROUP_2:70; :: thesis: verum

end;

end;