let p, q, p1 be Point of (TOP-REAL 2); :: thesis: ( p `1 <= q `1 & q `1 <= p1 `1 & p `2 = q `2 & q `2 = p1 `2 implies q in LSeg (p,p1) )
assume that
A1: ( p `1 <= q `1 & q `1 <= p1 `1 ) and
A2: p `2 = q `2 and
A3: q `2 = p1 `2 ; :: thesis: q in LSeg (p,p1)
A4: p `1 <= p1 `1 by A1, XXREAL_0:2;

per cases ( p `1 = p1 `1 or p `1 < p1 `1 ) by A4, XXREAL_0:1;

suppose A5: p `1 = p1 `1 ; :: thesis: q in LSeg (p,p1)

then p `1 = q `1 by A1, XXREAL_0:1;
then A6: q = |[(p `1),(p `2)]| by A2, EUCLID:53
.= p by EUCLID:53 ;
p = |[(p1 `1),(p1 `2)]| by A2, A3, A5, EUCLID:53
.= p1 by EUCLID:53 ;
then LSeg (p,p1) = {p} by RLTOPSP1:70;
hence q in LSeg (p,p1) by A6, TARSKI:def 1; :: thesis: verum

end;

suppose A7: p `1 < p1 `1 ; :: thesis: q in LSeg (p,p1)

A8: q in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = q `2 & p `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A1;
( p = |[(p `1),(q `2)]| & p1 = |[(p1 `1),(q `2)]| ) by A2, A3, EUCLID:53;
hence q in LSeg (p,p1) by A7, A8, TOPREAL3:10; :: thesis: verum

end;

end;