let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & LSeg (q1,q2) c= LSeg (p1,p2) & not q1 `1 = q2 `1 implies q1 `2 = q2 `2 )
A1:
q2 in LSeg (q1,q2)
by RLTOPSP1:68;
q1 in LSeg (q1,q2)
by RLTOPSP1:68;
hence
( ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & LSeg (q1,q2) c= LSeg (p1,p2) & not q1 `1 = q2 `1 implies q1 `2 = q2 `2 )
by A1, Th2; verum