let S be IncProjStr ; :: thesis: for F being IncProjMap over 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 over 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 that
A1: F is incidence_preserving and
A2: K is clique ; :: thesis: F .: K is clique
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 that
A3: B1 in F .: K and
A4: B2 in F .: K ; :: thesis: ex L being LINE of S st {B1,B2} on L
A5: F .: K = { B where B is POINT of S : ex A being POINT of S st
( A in K & F . A = B ) } by Th18;
then consider B11 being POINT of S such that
A6: B1 = B11 and
A7: ex A being POINT of S st
( A in K & F . A = B11 ) by A3;
consider B12 being POINT of S such that
A8: B2 = B12 and
A9: ex A being POINT of S st
( A in K & F . A = B12 ) by A5, A4;
consider A12 being POINT of S such that
A10: A12 in K and
A11: F . A12 = B12 by A9;
consider A11 being POINT of S such that
A12: A11 in K and
A13: F . A11 = B11 by A7;
consider L1 being LINE of S such that
A14: {A11,A12} on L1 by A2, A12, A10;
A12 on L1 by A14, INCSP_1:1;
then A15: F . A12 on F . L1 by A1;
A11 on L1 by A14, INCSP_1:1;
then F . A11 on F . L1 by A1;
then {B1,B2} on F . L1 by A6, A8, A13, A11, A15, INCSP_1:1;
hence ex L being LINE of S st {B1,B2} on L ; :: thesis: verum