let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n) holds p in halfline p,q
let p, q be Point of (TOP-REAL n); :: thesis: p in halfline p,q
((1 - 0 ) * p) + (0 * q) = p + (0 * q) by EUCLID:33
.= p + (0. (TOP-REAL n)) by EUCLID:33
.= p by EUCLID:31 ;
hence p in halfline p,q ; :: thesis: verum