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

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))

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;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

now :: thesis: for x being object st x in rng (IncProj (A,o,B)) holds

x in CHAIN B

hence
rng (IncProj (A,o,B)) = CHAIN B
by A2, TARSKI:2; :: thesis: verumx 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;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