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
dom (IncProj A,o,B) = CHAIN A
let o be POINT of IPP; :: thesis: for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj A,o,B) = CHAIN A
let A, B be LINE of IPP; :: thesis: ( not o on A & not o on B implies dom (IncProj A,o,B) = CHAIN A )
assume A1: ( not o on A & not o on B ) ; :: thesis: dom (IncProj A,o,B) = CHAIN A

A2: now

let x be set ; :: thesis: ( x in dom (IncProj A,o,B) implies x in CHAIN A )
assume A3: x in dom (IncProj A,o,B) ; :: thesis: x in CHAIN A
then reconsider x' = x as POINT of IPP ;
x' on A by A1, A3, PROJRED1:def 1;
hence x in CHAIN A ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in CHAIN A implies x in dom (IncProj A,o,B) )
assume x in CHAIN A ; :: thesis: x in dom (IncProj A,o,B)
then ex b being POINT of IPP st
( b = x & b on A ) ;
hence x in dom (IncProj A,o,B) by A1, PROJRED1:def 1; :: thesis: verum

end;

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