let S be IncProjStr ; :: thesis: for F being IncProjMap of 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 )
let F be IncProjMap of S,S; :: thesis: 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 )
let K be Subset of the Points of S; :: thesis: ( F is automorphism & K is maximal_clique implies ( F .: K is maximal_clique & F " K is maximal_clique ) )
assume that
A1: F is automorphism and
A2: K is maximal_clique ; :: thesis: ( F .: K is maximal_clique & F " K is maximal_clique )
A3: F is incidence_preserving by A1, Def9;
the point-map of F is bijective by A1, Def9;
then A4: the Points of S = rng the point-map of F by FUNCT_2:def 3;
A5: the Points of S = dom the point-map of F by FUNCT_2:52;
A6: for U being Subset of the Points of S st U is clique & F " K c= U holds
U = F " K

proof

let U be Subset of the Points of S; :: thesis: ( U is clique & F " K c= U implies U = F " K )
assume that
A7: U is clique and
A8: F " K c= U ; :: thesis: U = F " K
F .: (F " K) c= F .: U by A8, RELAT_1:123;
then A9: K c= F .: U by A4, FUNCT_1:77;
A10: U c= F " (F .: U) by A5, FUNCT_1:76;
F .: U is clique by A3, A7, Th20;
then U c= F " K by A2, A9, A10, Def3;
hence U = F " K by A8, XBOOLE_0:def 10; :: thesis: verum

end;

A11: the line-map of F is bijective by A1, Def9;
A12: for U being Subset of the Points of S st U is clique & F .: K c= U holds
U = F .: K

proof

A13: K c= F " (F .: K) by A5, FUNCT_1:76;
let U be Subset of the Points of S; :: thesis: ( U is clique & F .: K c= U implies U = F .: K )
assume that
A14: U is clique and
A15: F .: K c= U ; :: thesis: U = F .: K
F " (F .: K) c= F " U by A15, RELAT_1:143;
then A16: K c= F " U by A13, XBOOLE_1:1;
F " U is clique by A11, A3, A14, Th21;
then F .: (F " U) c= F .: K by A2, A16, Def3;
then U c= F .: K by A4, FUNCT_1:77;
hence U = F .: K by A15, XBOOLE_0:def 10; :: thesis: verum

end;

A17: K is clique by A2, Def3;
then A18: F .: K is clique by A3, Th20;
F " K is clique by A11, A17, A3, Th21;
hence ( F .: K is maximal_clique & F " K is maximal_clique ) by A18, A12, A6, Def3; :: thesis: verum