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 :: thesis: for x being object st x in dom (IncProj (A,o,B)) holds
x in CHAIN A
let x be object ; :: 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 x9 = x as POINT of IPP ;
x9 on A by A1, A3, PROJRED1:def 1;
hence x in CHAIN A ; :: thesis: verum
end;
now :: thesis: for x being object st x in CHAIN A holds
x in dom (IncProj (A,o,B))
let x be object ; :: 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