let n be Element of NAT ; :: thesis: for p, q being Point of (TOP-REAL n)
for x being set holds
( x in halfline (p,q) iff ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) )
let p, q be Point of (TOP-REAL n); :: thesis: for x being set holds
( x in halfline (p,q) iff ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) )
let x be set ; :: thesis: ( x in halfline (p,q) iff ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) )

hereby :: thesis: ( ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) implies x in halfline (p,q) )

assume x in halfline (p,q) ; :: thesis: ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l )
then ex l being Real st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) ;
hence ex l being real number st
( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; :: thesis: verum

end;

given l being real number such that A1: ( x = ((1 - l) * p) + (l * q) & 0 <= l ) ; :: thesis: x in halfline (p,q)
l is Real by XREAL_0:def 1;
hence x in halfline (p,q) by A1; :: thesis: verum