for Gc being finite strict cyclic Group st ex k being Element of NAT st card Gc = 2 * k holds
ex H being Subgroup of Gc st
( card H = 2 & H is cyclic Group )