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:69;
q1 in LSeg q1,q2
by RLTOPSP1:69;
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, Th35; verum