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

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

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;

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

then p in {|[r,r1]|} by A1, RLTOPSP1:70;
then p = |[r,r1]| by TARSKI:def 1;
hence p `1 = r ; :: thesis: verum

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 & s1 <= q `2 & q `2 <= r1 ) } by Th9;
then ex p1 being Point of (TOP-REAL 2) st
( p1 = p & p1 `1 = r & s1 <= p1 `2 & p1 `2 <= r1 ) by A1;
hence p `1 = r ; :: thesis: verum

end;

end;