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 rng (IncProj A,o,B) implies x in CHAIN B )
assume A3: 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 x' = x as POINT of IPP by A3;
x' on B by A1, A3, PROJRED1:24;
hence x in CHAIN B ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in CHAIN B implies x in rng (IncProj A,o,B) )
assume A4: x in CHAIN B ; :: thesis: x in rng (IncProj A,o,B)
then A5: ex b being POINT of IPP st
( b = x & b on B ) ;
reconsider x' = x as Element of the Points of IPP by A4;
consider y being POINT of IPP such that
A6: ( y on A & (IncProj A,o,B) . y = x' ) by A1, A5, Th3;
y in dom (IncProj A,o,B)

proof

y in CHAIN A by A6;
hence y in dom (IncProj A,o,B) by A1, Th5; :: thesis: verum

end;

hence x in rng (IncProj A,o,B) by A6, FUNCT_1:def 5; :: thesis: verum

end;

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