let n be Element of NAT ; :: thesis: for p being Point of (TOP-REAL n) holds halfline (p,p) = {p}
let p be Point of (TOP-REAL n); :: thesis: halfline (p,p) = {p}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {p} c= halfline (p,p)

let d be set ; :: thesis: ( d in halfline (p,p) implies d in {p} )
assume d in halfline (p,p) ; :: thesis: d in {p}
then ex r being real number st
( d = ((1 - r) * p) + (r * p) & 0 <= r ) by Th26;
then d = p by Th4;
hence d in {p} by TARSKI:def 1; :: thesis: verum

end;

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in {p} or d in halfline (p,p) )
assume d in {p} ; :: thesis: d in halfline (p,p)
then d = p by TARSKI:def 1;
hence d in halfline (p,p) by Th27; :: thesis: verum