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 ) )
A1: q1 in LSeg q1,q2 by RLTOPSP1:69;
A2: q2 in LSeg q1,q2 by RLTOPSP1:69;
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, Th24, RLTOPSP1:69;

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 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:71;
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;