let n be Element of NAT ; :: thesis: for x1, x2, x3 being Element of REAL n
for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane x1,x2,x3
let x1, x2, x3 be Element of REAL n; :: thesis: for P being Element of plane_of_REAL n st x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 holds
P = plane x1,x2,x3
let P be Element of plane_of_REAL n; :: thesis: ( x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 implies P = plane x1,x2,x3 )
assume A1: ( x1 in P & x2 in P & x3 in P & x2 - x1,x3 - x1 are_lindependent2 ) ; :: thesis: P = plane x1,x2,x3
P in plane_of_REAL n ;
then consider P' being Subset of (REAL n) such that
A2: ( P = P' & ex y1, y2, y3 being Element of REAL n st P' = plane y1,y2,y3 ) ;
consider y1, y2, y3 being Element of REAL n such that
A3: P = plane y1,y2,y3 by A2;
A4: plane x1,x2,x3 c= P by A1, A3, Th88;
consider x' being Element of REAL n such that
A5: ( x1 = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * y1) + (a2' * y2)) + (a3' * y3) ) ) by A1, A3;
consider a11, a12, a13 being Real such that
A6: ( (a11 + a12) + a13 = 1 & x1 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) by A5;
consider x' being Element of REAL n such that
A7: ( x2 = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * y1) + (a2' * y2)) + (a3' * y3) ) ) by A1, A3;
consider a21, a22, a23 being Real such that
A8: ( (a21 + a22) + a23 = 1 & x2 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) by A7;
consider x' being Element of REAL n such that
A9: ( x3 = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * y1) + (a2' * y2)) + (a3' * y3) ) ) by A1, A3;
consider a31, a32, a33 being Real such that
A10: ( (a31 + a32) + a33 = 1 & x3 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) by A9;
A11: x1 = (y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)) by A6, Th32;
A12: x3 = (y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1)) by A10, Th32;
A13: x2 - x1 = ((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + (- ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)))) by A8, A11, Th32
.= ((y1 + (a22 * (y2 - y1))) + (a23 * (y3 - y1))) + (((- y1) + (- (a12 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) by Th13
.= ((y1 + (- y1)) + ((a22 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th22
.= ((0* n) + ((a22 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th7
.= ((0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th16
.= ((0* n) + ((a22 - a12) * (y2 - y1))) + ((a23 - a13) * (y3 - y1)) by Th16
.= ((a22 - a12) * (y2 - y1)) + ((a23 - a13) * (y3 - y1)) by EUCLID_4:1 ;
x3 - x1 = ((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + (- ((y1 + (a12 * (y2 - y1))) + (a13 * (y3 - y1)))) by A6, A12, Th32
.= ((y1 + (a32 * (y2 - y1))) + (a33 * (y3 - y1))) + (((- y1) + (- (a12 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) by Th13
.= ((y1 + (- y1)) + ((a32 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th22
.= ((0* n) + ((a32 * (y2 - y1)) + (- (a12 * (y2 - y1))))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th7
.= ((0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 * (y3 - y1)) + (- (a13 * (y3 - y1)))) by Th16
.= ((0* n) + ((a32 - a12) * (y2 - y1))) + ((a33 - a13) * (y3 - y1)) by Th16
.= ((a32 - a12) * (y2 - y1)) + ((a33 - a13) * (y3 - y1)) by EUCLID_4:1 ;
then consider c1, c2, d1, d2 being Real such that
A14: ( y2 - y1 = (c1 * (x2 - x1)) + (c2 * (x3 - x1)) & y3 - y1 = (d1 * (x2 - x1)) + (d2 * (x3 - x1)) ) by A1, A13, Th41;
A15: x1 = y1 + ((a12 * (y2 - y1)) + (a13 * (y3 - y1))) by A11, RVSUM_1:32;

now

let y be set ; :: thesis: ( y in P implies y in plane x1,x2,x3 )
assume y in P ; :: thesis: y in plane x1,x2,x3
then consider x' being Element of REAL n such that
A16: ( y = x' & ex a1', a2', a3' being Real st
( (a1' + a2') + a3' = 1 & x' = ((a1' * y1) + (a2' * y2)) + (a3' * y3) ) ) by A3;
consider b1, b2, b3 being Real such that
A17: ( (b1 + b2) + b3 = 1 & y = ((b1 * y1) + (b2 * y2)) + (b3 * y3) ) by A16;
y = (y1 + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by A17, Th32
.= ((x1 - ((a12 * (y2 - y1)) + (a13 * (y3 - y1)))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by A15, Th11
.= (((x1 - (a12 * (y2 - y1))) - (a13 * (y3 - y1))) + (b2 * (y2 - y1))) + (b3 * (y3 - y1)) by RVSUM_1:60
.= (((x1 + (- (a12 * (y2 - y1)))) + (b2 * (y2 - y1))) + (- (a13 * (y3 - y1)))) + (b3 * (y3 - y1)) by RVSUM_1:32
.= ((x1 + ((- (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + (- (a13 * (y3 - y1)))) + (b3 * (y3 - y1)) by RVSUM_1:32
.= (x1 + ((- (a12 * (y2 - y1))) + (b2 * (y2 - y1)))) + ((- (a13 * (y3 - y1))) + (b3 * (y3 - y1))) by RVSUM_1:32
.= (x1 + ((b2 - a12) * (y2 - y1))) + ((- (a13 * (y3 - y1))) + (b3 * (y3 - y1))) by Th16
.= (x1 + ((b2 - a12) * (y2 - y1))) + ((b3 - a13) * (y3 - y1)) by Th16
.= (x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + ((b3 - a13) * ((d1 * (x2 - x1)) + (d2 * (x3 - x1)))) by A14, EUCLID_4:6
.= (x1 + (((b2 - a12) * (c1 * (x2 - x1))) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:6
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + ((b2 - a12) * (c2 * (x3 - x1))))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + (((b3 - a13) * (d1 * (x2 - x1))) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + ((b3 - a13) * (d2 * (x3 - x1)))) by EUCLID_4:4
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b2 - a12) * c2) * (x3 - x1)))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by EUCLID_4:4
.= ((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + ((((b3 - a13) * d1) * (x2 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1:32
.= (((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:32
.= (((x1 + (((b2 - a12) * c1) * (x2 - x1))) + (((b3 - a13) * d1) * (x2 - x1))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:32
.= ((x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + (((b2 - a12) * c2) * (x3 - x1))) + (((b3 - a13) * d2) * (x3 - x1)) by RVSUM_1:32
.= (x1 + ((((b2 - a12) * c1) * (x2 - x1)) + (((b3 - a13) * d1) * (x2 - x1)))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by RVSUM_1:32
.= (x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) * (x3 - x1)) + (((b3 - a13) * d2) * (x3 - x1))) by EUCLID_4:7
.= (x1 + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * (x2 - x1))) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * (x3 - x1)) by EUCLID_4:7 ;
then consider a being Real such that
A18: ( y = ((a * x1) + ((((b2 - a12) * c1) + ((b3 - a13) * d1)) * x2)) + ((((b2 - a12) * c2) + ((b3 - a13) * d2)) * x3) & (a + (((b2 - a12) * c1) + ((b3 - a13) * d1))) + (((b2 - a12) * c2) + ((b3 - a13) * d2)) = 1 ) by Th33;
thus y in plane x1,x2,x3 by A18; :: thesis: verum

end;

then P c= plane x1,x2,x3 by TARSKI:def 3;
hence P = plane x1,x2,x3 by A4, XBOOLE_0:def 10; :: thesis: verum