let S be IncProjStr ; :: thesis: 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 )

let F be IncProjMap over 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;

the point-map of F is bijective by A1;

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

A12: for U being Subset of the Points of S st U is clique & F .: K c= U holds

U = F .: K

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; :: thesis: verum

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 over 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;

the point-map of F is bijective by A1;

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

A11:
the line-map of F is bijective
by A1;
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;

hence U = F " K by A8, XBOOLE_0:def 10; :: thesis: verum

end;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;

hence U = F " K by A8, XBOOLE_0:def 10; :: thesis: verum

A12: for U being Subset of the Points of S st U is clique & F .: K c= U holds

U = F .: K

proof

A17:
K is clique
by A2;
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;

F " U is clique by A11, A3, A14, Th21;

then F .: (F " U) c= F .: K by A2, A16;

then U c= F .: K by A4, FUNCT_1:77;

hence U = F .: K by A15, XBOOLE_0:def 10; :: thesis: verum

end;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;

F " U is clique by A11, A3, A14, Th21;

then F .: (F " U) c= F .: K by A2, A16;

then U c= F .: K by A4, FUNCT_1:77;

hence U = F .: K by A15, XBOOLE_0:def 10; :: thesis: verum

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; :: thesis: verum