let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis: for o being POINT of
for A, B being LINE of st not o on A & not o on B holds
(IncProj A,o,B) " = IncProj B,o,A
let o be POINT of ; :: thesis: for A, B being LINE of st not o on A & not o on B holds
(IncProj A,o,B) " = IncProj B,o,A
let A, B be LINE of ; :: thesis: ( not o on A & not o on B implies (IncProj A,o,B) " = IncProj B,o,A )
set f = IncProj A,o,B;
set g = IncProj B,o,A;
assume A1: ( not o on A & not o on B ) ; :: thesis: (IncProj A,o,B) " = IncProj B,o,A
then A2: rng (IncProj A,o,B) = CHAIN B by Th6;
A3: dom (IncProj A,o,B) = CHAIN A by A1, Th5;

A4: now

let y, x be set ; :: thesis: ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y iff ( x in dom (IncProj A,o,B) & y = (IncProj A,o,B) . x ) )

A5: now

assume that
A6: x in dom (IncProj A,o,B) and
A7: y = (IncProj A,o,B) . x ; :: thesis: ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y )
consider x' being POINT of such that
A8: ( x = x' & x' on A ) by A3, A6;
reconsider y' = y as POINT of by A1, A7, A8, PROJRED1:22;
A9: y' on B by A1, A7, A8, PROJRED1:23;
then A10: y in CHAIN B ;
ex O being LINE of st
( o on O & x' on O & y' on O ) by A1, A7, A8, A9, PROJRED1:def 1;
hence ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y ) by A1, A8, A9, A10, Th6, PROJRED1:def 1; :: thesis: verum

end;

now

assume that
A11: y in rng (IncProj A,o,B) and
A12: x = (IncProj B,o,A) . y ; :: thesis: ( x in dom (IncProj A,o,B) & y = (IncProj A,o,B) . x )
consider y' being POINT of such that
A13: ( y = y' & y' on B ) by A2, A11;
reconsider x' = x as POINT of by A1, A12, A13, PROJRED1:22;
A14: x' on A by A1, A12, A13, PROJRED1:23;
then ex O being LINE of st
( o on O & y' on O & x' on O ) by A1, A12, A13, PROJRED1:def 1;
hence ( x in dom (IncProj A,o,B) & y = (IncProj A,o,B) . x ) by A1, A13, A14, PROJRED1:def 1; :: thesis: verum

end;

hence ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y iff ( x in dom (IncProj A,o,B) & y = (IncProj A,o,B) . x ) ) by A5; :: thesis: verum

end;

A15: IncProj A,o,B is one-to-one by A1, Th8;
dom (IncProj B,o,A) = CHAIN B by A1, Th5
.= rng (IncProj A,o,B) by A1, Th6 ;
hence (IncProj A,o,B) " = IncProj B,o,A by A15, A4, FUNCT_1:54; :: thesis: verum