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