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;

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;

end;

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;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

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;( 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