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 & the line-map of F is onto & 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 & the line-map of F is onto & K is clique holds

F " K is clique

let K be Subset of the Points of S; :: thesis: ( F is incidence_preserving & the line-map of F is onto & K is clique implies F " K is clique )

assume that

A1: F is incidence_preserving and

A2: the line-map of F is onto and

A3: K is clique ; :: thesis: F " K is clique

let A1, A2 be POINT of S; :: according to COMBGRAS:def 2 :: thesis: ( A1 in F " K & A2 in F " K implies ex L being LINE of S st {A1,A2} on L )

assume ( A1 in F " K & A2 in F " K ) ; :: thesis: ex L being LINE of S st {A1,A2} on L

then ( F . A1 in K & F . A2 in K ) by FUNCT_1:def 7;

then consider L2 being LINE of S such that

A4: {(F . A1),(F . A2)} on L2 by A3;

the Lines of S = rng the line-map of F by A2, FUNCT_2:def 3;

then consider l1 being object such that

A5: l1 in dom the line-map of F and

A6: L2 = the line-map of F . l1 by FUNCT_1:def 3;

consider L1 being LINE of S such that

A7: L1 = l1 by A5;

A8: L2 = F . L1 by A6, A7;

F . A2 on L2 by A4, INCSP_1:1;

then A9: A2 on L1 by A1, A8;

F . A1 on L2 by A4, INCSP_1:1;

then A1 on L1 by A1, A8;

then {A1,A2} on L1 by A9, INCSP_1:1;

hence ex L being LINE of S st {A1,A2} on L ; :: thesis: verum

for K being Subset of the Points of S st F is incidence_preserving & the line-map of F is onto & 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 & the line-map of F is onto & K is clique holds

F " K is clique

let K be Subset of the Points of S; :: thesis: ( F is incidence_preserving & the line-map of F is onto & K is clique implies F " K is clique )

assume that

A1: F is incidence_preserving and

A2: the line-map of F is onto and

A3: K is clique ; :: thesis: F " K is clique

let A1, A2 be POINT of S; :: according to COMBGRAS:def 2 :: thesis: ( A1 in F " K & A2 in F " K implies ex L being LINE of S st {A1,A2} on L )

assume ( A1 in F " K & A2 in F " K ) ; :: thesis: ex L being LINE of S st {A1,A2} on L

then ( F . A1 in K & F . A2 in K ) by FUNCT_1:def 7;

then consider L2 being LINE of S such that

A4: {(F . A1),(F . A2)} on L2 by A3;

the Lines of S = rng the line-map of F by A2, FUNCT_2:def 3;

then consider l1 being object such that

A5: l1 in dom the line-map of F and

A6: L2 = the line-map of F . l1 by FUNCT_1:def 3;

consider L1 being LINE of S such that

A7: L1 = l1 by A5;

A8: L2 = F . L1 by A6, A7;

F . A2 on L2 by A4, INCSP_1:1;

then A9: A2 on L1 by A1, A8;

F . A1 on L2 by A4, INCSP_1:1;

then A1 on L1 by A1, A8;

then {A1,A2} on L1 by A9, INCSP_1:1;

hence ex L being LINE of S st {A1,A2} on L ; :: thesis: verum