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:57
.= p by EUCLID:57 ;
p = |[(p1 `1 ),(p1 `2 )]| by A2, A3, 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 `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:57;
hence q in LSeg p,p1 by A7, A8, TOPREAL3:16; :: thesis: verum

end;

end;