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 & the line-map of F is onto & 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 & 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 A1: ( F is incidence_preserving & the line-map of F is onto & K is clique ) ; :: thesis: F " K is clique
then A2: ( the Points of S = dom the point-map of F & the Lines of S = rng the line-map of F & the Lines of S = dom the line-map of F ) by FUNCT_2:67, FUNCT_2:def 3;
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 A3: ( A1 in F " K & A2 in F " K ) ; :: thesis: ex L being LINE of S st {A1,A2} on L
( A1 in dom the point-map of F & F . A1 in K & A2 in dom the point-map of F & F . A2 in K ) by A3, FUNCT_1:def 13;
then consider L2 being LINE of S such that
A4: {(F . A1),(F . A2)} on L2 by A1, Def2;
A5: ( F . A1 on L2 & F . A2 on L2 & L2 in rng the line-map of F ) by A2, A4, INCSP_1:11;
consider l1 being set such that
A6: ( l1 in dom the line-map of F & L2 = the line-map of F . l1 ) by A2, FUNCT_1:def 5;
consider L1 being LINE of S such that
A7: L1 = l1 by A6;
L2 = F . L1 by A6, A7;
then ( A1 on L1 & A2 on L1 ) by A1, A5, Def8;
then {A1,A2} on L1 by INCSP_1:11;
hence ex L being LINE of S st {A1,A2} on L ; :: thesis: verum