let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B
let o be POINT of IPP; :: thesis: for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B
let A, B be LINE of IPP; :: thesis: ( not o on A & not o on B implies rng (IncProj (A,o,B)) = CHAIN B )
assume A1: ( not o on A & not o on B ) ; :: thesis: rng (IncProj (A,o,B)) = CHAIN B
A2: now :: thesis: for x being object st x in CHAIN B holds
x in rng (IncProj (A,o,B))
let x be object ; :: thesis: ( x in CHAIN B implies x in rng (IncProj (A,o,B)) )
assume A3: x in CHAIN B ; :: thesis: x in rng (IncProj (A,o,B))
then reconsider x9 = x as Element of the Points of IPP ;
ex b being POINT of IPP st
( b = x & b on B ) by A3;
then consider y being POINT of IPP such that
A4: y on A and
A5: (IncProj (A,o,B)) . y = x9 by A1, Th3;
y in CHAIN A by A4;
then y in dom (IncProj (A,o,B)) by A1, Th4;
hence x in rng (IncProj (A,o,B)) by A5, FUNCT_1:def 3; :: thesis: verum
end;
now :: thesis: for x being object st x in rng (IncProj (A,o,B)) holds
x in CHAIN B
let x be object ; :: thesis: ( x in rng (IncProj (A,o,B)) implies x in CHAIN B )
assume A6: x in rng (IncProj (A,o,B)) ; :: thesis: x in CHAIN B
rng (IncProj (A,o,B)) c= the Points of IPP by RELAT_1:def 19;
then reconsider x9 = x as POINT of IPP by A6;
x9 on B by A1, A6, PROJRED1:21;
hence x in CHAIN B ; :: thesis: verum
end;
hence rng (IncProj (A,o,B)) = CHAIN B by A2, TARSKI:2; :: thesis: verum