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:52;
hence a in halfline p,q ; :: thesis: verum