let p be Point of (TOP-REAL 2); :: thesis: for r, r1, s1 being Real st p in LSeg (|[r,r1]|,|[r,s1]|) holds

p `1 = r

let r, r1, s1 be Real; :: thesis: ( p in LSeg (|[r,r1]|,|[r,s1]|) implies p `1 = r )

assume A1: p in LSeg (|[r,r1]|,|[r,s1]|) ; :: thesis: p `1 = r

p `1 = r

let r, r1, s1 be Real; :: thesis: ( p in LSeg (|[r,r1]|,|[r,s1]|) implies p `1 = r )

assume A1: p in LSeg (|[r,r1]|,|[r,s1]|) ; :: thesis: p `1 = r

per cases
( r1 < s1 or r1 = s1 or r1 > s1 )
by XXREAL_0:1;

end;

suppose
r1 < s1
; :: thesis: p `1 = r

then
LSeg (|[r,r1]|,|[r,s1]|) = { q where q is Point of (TOP-REAL 2) : ( q `1 = r & r1 <= q `2 & q `2 <= s1 ) }
by Th9;

then ex p1 being Point of (TOP-REAL 2) st

( p1 = p & p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) by A1;

hence p `1 = r ; :: thesis: verum

end;then ex p1 being Point of (TOP-REAL 2) st

( p1 = p & p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) by A1;

hence p `1 = r ; :: thesis: verum