theorem Th23: :: COMBGRAS:23

for k being Element of NAT
for X being non empty set st 2 <= k & k + 2 c= card X holds
for F being IncProjMap over G_ (k,X), G_ (k,X) st F is automorphism holds
for K being Subset of the Points of (G_ (k,X)) st K is STAR holds
( F .: K is STAR & F " K is STAR )