let p be Point of (TOP-REAL 2); :: thesis: for r, r1, s1 being real number st p in LSeg |[r,r1]|,|[r,s1]| holds
p `1 = r
let r, r1, s1 be real number ; :: 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 Th15;
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:71;
then p = |[r,r1]| by TARSKI:def 1;
hence p `1 = r by EUCLID:56; :: 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 Th15;
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;