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 and
A2: q `1 = p1 `1 and
A3: ( p `2 <= q `2 & q `2 <= p1 `2 ) ; :: thesis: q in LSeg p,p1
A4: p `2 <= p1 `2 by A3, XXREAL_0:2;

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

suppose A5: p `2 = p1 `2 ; :: thesis: q in LSeg p,p1

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

end;

suppose A7: p `2 < p1 `2 ; :: thesis: q in LSeg p,p1

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

end;

end;