A1: 0 * x3 = 0* n by EUCLID_4:3;
A2: (1 + 0) + 0 = 1 ;
( 1 * x1 = x1 & 0 * x2 = 0* n ) by EUCLID_4:3;
then ((1 * x1) + (0 * x2)) + (0 * x3) = x1 + (0* n) by A1, EUCLID_4:1
.= x1 by EUCLID_4:1 ;
then x1 in plane (x1,x2,x3) by A2;
hence not plane (x1,x2,x3) is empty ; :: thesis: verum