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