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 11;
gr {(b |^ 2)} <> G

proof

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:25;
b = b |^ (2 * j1) by A8, GROUP_1:67;
then (b " ) * (b |^ (2 * j1)) = 1_ G by GROUP_1:def 6;
then (b |^ (- 1)) * (b |^ (2 * j1)) = 1_ G by GROUP_1:62;
then b |^ ((- 1) + (2 * j1)) = 1_ G by GROUP_1:63;
then (- 1) + (2 * j1) = 0 by A6, Th13;
hence contradiction by INT_1:22; :: thesis: verum

end;

hence gr {(b |^ 2)} <> G by A4, GR_CY_2:8; :: thesis: verum

end;

hence contradiction by A2, A7, Th7; :: thesis: verum

end;

then consider n being Element of NAT such that
A9: ( n = ord b & 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:27;
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 natural number st
( m divides n & not m = 1 & not m = n ) ) by A12, INT_2:def 5;
A14: n > 1

proof

A15: n >= 1 by A10, A11, GROUP_1:90;
n <> 1 by A3, A9, GROUP_1:85;
hence n > 1 by A15, XXREAL_0:1; :: thesis: verum

end;

then consider m being natural number such that
A16: ( m <> 1 & m <> n & m divides n ) by A13;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
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 13;
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 )
A18: u > 1

proof

u <> 0

proof

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

end;

then 0 < u ;
then 0 + 1 <= u by INT_1:20;
hence u > 1 by A16, XXREAL_0:1; :: thesis: verum

end;

v > 1

proof

v <> 0 by A14, A17;
then 0 < v ;
then A19: 0 + 1 <= v by INT_1:20;
v <> 1 by A16, A17;
hence v > 1 by A19, XXREAL_0:1; :: thesis: verum

end;

hence ( u > 1 & v > 1 & n = u * v ) by A17, A18; :: thesis: verum

end;

then consider u, v being Element of NAT such that
A20: ( u > 1 & v > 1 & n = u * v ) ;
ord (b |^ v) = u by A4, A10, A11, A20, GR_CY_2:14;
then A21: card (gr {(b |^ v)}) = u by A10, GR_CY_1:27;
A22: u <> n by A20, XCMPLX_1:7;
gr {(b |^ v)} <> (1). G by A20, A21, GROUP_2:81;
hence contradiction by A2, A11, A21, A22; :: 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:10; :: thesis: verum

end;

assume A23: ( G is cyclic & G is finite & 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 A23;
reconsider H = H as Subgroup of G ;
card G = (card H) * (index H) by GROUP_2:177;
then A24: card H divides card G by NAT_D:def 3;

per cases ( card H = card G or card H = 1 ) by A23, A24, INT_2:def 5;

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

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

end;

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

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

end;

end;