( 1 - 0 = 1 & 1 * p1 = p1 & 0 * p2 = 0.REAL n & p1 + (0.REAL n) = p1 ) by EUCLID:31, EUCLID:33;
then p1 in Line p1,p2 ;
hence not Line p1,p2 is empty ; :: thesis: verum