let S be IncProjStr ; :: thesis: for F being IncProjMap of S,S
for K being Subset of the Points of S st F is incidence_preserving & K is clique holds
F .: K is clique
let F be IncProjMap of S,S; :: thesis: for K being Subset of the Points of S st F is incidence_preserving & K is clique holds
F .: K is clique
let K be Subset of the Points of S; :: thesis: ( F is incidence_preserving & K is clique implies F .: K is clique )
assume A1: ( F is incidence_preserving & K is clique ) ; :: thesis: F .: K is clique
A2: F .: K = { B where B is POINT of S : ex A being POINT of S st
( A in K & F . A = B ) } by Th18;
let B1, B2 be POINT of S; :: according to COMBGRAS:def 2 :: thesis: ( B1 in F .: K & B2 in F .: K implies ex L being LINE of S st {B1,B2} on L )
assume A3: ( B1 in F .: K & B2 in F .: K ) ; :: thesis: ex L being LINE of S st {B1,B2} on L
then consider B11 being POINT of S such that
A4: ( B1 = B11 & ex A being POINT of S st
( A in K & F . A = B11 ) ) by A2;
consider B12 being POINT of S such that
A5: ( B2 = B12 & ex A being POINT of S st
( A in K & F . A = B12 ) ) by A2, A3;
consider A11 being POINT of S such that
A6: ( A11 in K & F . A11 = B11 ) by A4;
consider A12 being POINT of S such that
A7: ( A12 in K & F . A12 = B12 ) by A5;
consider L1 being LINE of S such that
A8: {A11,A12} on L1 by A1, A6, A7, Def2;
( A11 on L1 & A12 on L1 ) by A8, INCSP_1:11;
then ( F . A11 on F . L1 & F . A12 on F . L1 ) by A1, Def8;
then {B1,B2} on F . L1 by A4, A5, A6, A7, INCSP_1:11;
hence ex L being LINE of S st {B1,B2} on L ; :: thesis: verum