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