let IPP be 2-dimensional Desarguesian IncProjSp; 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; 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; ( 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 )
; rng (IncProj (A,o,B)) = CHAIN B
A2:
now for x being object st x in CHAIN B holds
x in rng (IncProj (A,o,B))let x be
object ;
( x in CHAIN B implies x in rng (IncProj (A,o,B)) )assume A3:
x in CHAIN B
;
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;
verum end;
hence
rng (IncProj (A,o,B)) = CHAIN B
by A2, TARSKI:2; verum