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

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