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

let x be set ; :: 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, Th5;
hence x in rng (IncProj A,o,B) by A5, FUNCT_1:def 5; :: thesis: verum

end;

now

let x be set ; :: 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:24;
hence x in CHAIN B ; :: thesis: verum

end;

hence rng (IncProj A,o,B) = CHAIN B by A2, TARSKI:2; :: thesis: verum