let V be RealLinearSpace; :: thesis: for p being Element of V holds halfline (p,p) = {p}
let p be Element of V; :: thesis: halfline (p,p) = {p}

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

let d be object ; :: 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 st
( d = ((1 - r) * p) + (r * p) & 0 <= r ) ;
then d = p by Th2;
hence d in {p} by TARSKI:def 1; :: thesis: verum

end;

let d be object ; :: 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 Th25; :: thesis: verum