let n be Element of 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 ) )
assume A1: LSeg p1,p2 = LSeg q1,q2 ; :: thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) )
A2: ( q1 in LSeg q1,q2 & q2 in LSeg q1,q2 ) by RLTOPSP1:69;
A3: ( p1 in LSeg p1,p2 & p2 in LSeg p1,p2 ) by RLTOPSP1:69;

per cases ( ( p1 = q1 & p2 = q1 ) or ( p1 = q2 & p2 = q2 ) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A1, A3, Th24;

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

then LSeg p1,p2 = {q1} by RLTOPSP1:71;
hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A1, 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:71;
hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A1, A2, 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;