((1 - 0) * p) + (0 * q) in halfline (p,q) ;
hence not halfline (p,q) is empty ; :: thesis: verum