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
(IncProj A,o,B) " = IncProj B,o,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
(IncProj A,o,B) " = IncProj B,o,A
let A, B be LINE of IPP; :: thesis: ( not o on A & not o on B implies (IncProj A,o,B) " = IncProj B,o,A )
assume A1: ( not o on A & not o on B ) ; :: thesis: (IncProj A,o,B) " = IncProj B,o,A
set f = IncProj A,o,B;
set g = IncProj B,o,A;
A2: IncProj A,o,B is one-to-one by A1, Th8;
A3: dom (IncProj B,o,A) = CHAIN B by A1, Th5
.= rng (IncProj A,o,B) by A1, Th6 ;
A4: ( dom (IncProj A,o,B) = CHAIN A & rng (IncProj A,o,B) = CHAIN B ) by A1, Th5, Th6;

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 ) )
thus ( 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 ) ) :: thesis: verum

proof

A5: now

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

end;

now

assume A9: ( x in dom (IncProj A,o,B) & y = (IncProj A,o,B) . x ) ; :: thesis: ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y )
then consider x' being POINT of IPP such that
A10: ( x = x' & x' on A ) by A4;
reconsider y' = y as POINT of IPP by A1, A9, A10, PROJRED1:22;
A11: y' on B by A1, A9, A10, PROJRED1:23;
then A12: ex O being LINE of IPP st
( o on O & x' on O & y' on O ) by A1, A9, A10, PROJRED1:def 1;
y in CHAIN B by A11;
hence ( y in rng (IncProj A,o,B) & x = (IncProj B,o,A) . y ) by A1, A10, A11, A12, Th6, 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;

end;

hence (IncProj A,o,B) " = IncProj B,o,A by A2, A3, FUNCT_1:54; :: thesis: verum