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 ;
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 ;
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 ;
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 ;
n >= 1 by ;
then n > 1 by ;
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 ;
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 ;
hence contradiction by A10, A11; :: thesis: verum
end;
then A18: 0 + 1 <= u by INT_1:7;
0 < v by ;
then A19: 0 + 1 <= v by INT_1:7;
v <> 1 by ;
hence ( u > 1 & v > 1 & n = u * v ) by ; :: 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 ;
then A23: card (gr {(b |^ v)}) = u by ;
A24: u <> n by ;
gr {(b |^ v)} <> (1). G by ;
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 ; :: 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) * () 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 ;
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;