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