let Gc be finite strict cyclic Group; :: thesis: ( ex k being Element of NAT st card Gc = 2 * k implies ex H being Subgroup of Gc st

( card H = 2 & H is cyclic Group ) )

set n = card Gc;

assume ex k being Element of NAT st card Gc = 2 * k ; :: thesis: ex H being Subgroup of Gc st

( card H = 2 & H is cyclic Group )

then consider g1 being Element of Gc such that

A1: ord g1 = 2 and

for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 by Th24;

take gr {g1} ; :: thesis: ( card (gr {g1}) = 2 & gr {g1} is cyclic Group )

thus ( card (gr {g1}) = 2 & gr {g1} is cyclic Group ) by A1, Th4, GR_CY_1:7; :: thesis: verum

( card H = 2 & H is cyclic Group ) )

set n = card Gc;

assume ex k being Element of NAT st card Gc = 2 * k ; :: thesis: ex H being Subgroup of Gc st

( card H = 2 & H is cyclic Group )

then consider g1 being Element of Gc such that

A1: ord g1 = 2 and

for g2 being Element of Gc st ord g2 = 2 holds

g1 = g2 by Th24;

take gr {g1} ; :: thesis: ( card (gr {g1}) = 2 & gr {g1} is cyclic Group )

thus ( card (gr {g1}) = 2 & gr {g1} is cyclic Group ) by A1, Th4, GR_CY_1:7; :: thesis: verum