theorem Th22: :: COMBGRAS:22

for S being IncProjStr
for F being IncProjMap over S,S
for K being Subset of the Points of S st F is automorphism & K is maximal_clique holds
( F .: K is maximal_clique & F " K is maximal_clique )