let n be Nat; :: thesis: for x1, x2, x3 being Element of REAL n holds
( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) )
let x1, x2, x3 be Element of REAL n; :: thesis: ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) )
A1: 0 * x3 = 0* n by EUCLID_4:3;
( 1 * x1 = x1 & 0 * x2 = 0* n ) by EUCLID_4:3;
then A2: ((1 * x1) + (0 * x2)) + (0 * x3) = x1 + (0* n) by A1, EUCLID_4:1
.= x1 by EUCLID_4:1 ;
A3: 0 * x3 = 0* n by EUCLID_4:3;
A4: 1 * x3 = x3 by EUCLID_4:3;
( 0 * x1 = 0* n & 0 * x2 = 0* n ) by EUCLID_4:3;
then A5: ((0 * x1) + (0 * x2)) + (1 * x3) = (0* n) + x3 by A4, EUCLID_4:1
.= x3 by EUCLID_4:1 ;
( 0 * x1 = 0* n & 1 * x2 = x2 ) by EUCLID_4:3;
then A6: ((0 * x1) + (1 * x2)) + (0 * x3) = x2 + (0* n) by A3, EUCLID_4:1
.= x2 by EUCLID_4:1 ;
(0 + 0) + 1 = 1 ;
hence ( x1 in plane (x1,x2,x3) & x2 in plane (x1,x2,x3) & x3 in plane (x1,x2,x3) ) by A2, A6, A5; :: thesis: verum