let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n) holds LSeg (p,q) c= halfline (p,q)
let p, q be Point of (TOP-REAL n); :: thesis: LSeg (p,q) c= halfline (p,q)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in LSeg (p,q) or a in halfline (p,q) )
assume a in LSeg (p,q) ; :: thesis: a in halfline (p,q)
then ex r being Real st
( 0 <= r & r <= 1 & a = ((1 - r) * p) + (r * q) ) by JGRAPH_1:35;
hence a in halfline (p,q) ; :: thesis: verum