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