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