let p be Point of (TOP-REAL 2); :: thesis: for r1, r, s1 being real number st p in LSeg |[r1,r]|,|[s1,r]| holds
p `2 = r
let r1, r, s1 be real number ; :: thesis: ( p in LSeg |[r1,r]|,|[s1,r]| implies p `2 = r )
assume A1: p in LSeg |[r1,r]|,|[s1,r]| ; :: thesis: p `2 = r

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

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

then LSeg |[r1,r]|,|[s1,r]| = { q where q is Point of (TOP-REAL 2) : ( q `2 = r & r1 <= q `1 & q `1 <= s1 ) } by Th16;
then ex p1 being Point of (TOP-REAL 2) st
( p1 = p & p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) by A1;
hence p `2 = r ; :: thesis: verum

end;

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

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

end;

suppose r1 > s1 ; :: thesis: p `2 = r

then LSeg |[r1,r]|,|[s1,r]| = { q where q is Point of (TOP-REAL 2) : ( q `2 = r & s1 <= q `1 & q `1 <= r1 ) } by Th16;
then ex p1 being Point of (TOP-REAL 2) st
( p1 = p & p1 `2 = r & s1 <= p1 `1 & p1 `1 <= r1 ) by A1;
hence p `2 = r ; :: thesis: verum

end;

end;