let n be Nat; :: thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds
( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )
let p1, p2, q1, q2 be Point of (TOP-REAL n); :: thesis: ( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )
A1: q1 in LSeg (q1,q2) by RLTOPSP1:68;
A2: q2 in LSeg (q1,q2) by RLTOPSP1:68;
assume A3: LSeg (p1,p2) = LSeg (q1,q2) ; :: thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

per cases ( ( p1 = q1 & p2 = q1 ) or ( p1 = q2 & p2 = q2 ) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, Th7, RLTOPSP1:68;

suppose A4: ( p1 = q1 & p2 = q1 ) ; :: thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

then LSeg (p1,p2) = {q1} by RLTOPSP1:70;
hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, A2, A4, TARSKI:def 1; :: thesis: verum

end;

suppose A5: ( p1 = q2 & p2 = q2 ) ; :: thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

then LSeg (p1,p2) = {q2} by RLTOPSP1:70;
hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, A1, A5, TARSKI:def 1; :: thesis: verum

end;

suppose ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) ; :: thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )

hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) ; :: thesis: verum

end;

end;