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