let n be Element of NAT ; :: thesis: for x1, y1, y2, y3, x2, x3 being Element of REAL n st x1 in plane y1,y2,y3 & x2 in plane y1,y2,y3 & x3 in plane y1,y2,y3 holds
plane x1,x2,x3 c= plane y1,y2,y3
let x1, y1, y2, y3, x2, x3 be Element of REAL n; :: thesis: ( x1 in plane y1,y2,y3 & x2 in plane y1,y2,y3 & x3 in plane y1,y2,y3 implies plane x1,x2,x3 c= plane y1,y2,y3 )
assume A1: ( x1 in plane y1,y2,y3 & x2 in plane y1,y2,y3 & x3 in plane y1,y2,y3 ) ; :: thesis: plane x1,x2,x3 c= plane y1,y2,y3
then consider x1' being Element of REAL n such that
A2: ( x1 = x1' & ex a11, a12, a13 being Real st
( (a11 + a12) + a13 = 1 & x1' = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) ) ;
consider a11, a12, a13 being Real such that
A3: ( (a11 + a12) + a13 = 1 & x1 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) by A2;
consider x2' being Element of REAL n such that
A4: ( x2 = x2' & ex a21, a22, a23 being Real st
( (a21 + a22) + a23 = 1 & x2' = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) ) by A1;
consider a21, a22, a23 being Real such that
A5: ( (a21 + a22) + a23 = 1 & x2 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) by A4;
consider x3' being Element of REAL n such that
A6: ( x3 = x3' & ex a31, a32, a33 being Real st
( (a31 + a32) + a33 = 1 & x3' = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) ) by A1;
consider a31, a32, a33 being Real such that
A7: ( (a31 + a32) + a33 = 1 & x3 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) by A6;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in plane x1,x2,x3 or x in plane y1,y2,y3 )
assume x in plane x1,x2,x3 ; :: thesis: x in plane y1,y2,y3
then consider x' being Element of REAL n such that
A8: ( x = x' & ex b1, b2, b3 being Real st
( (b1 + b2) + b3 = 1 & x' = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ) ) ;
consider b1, b2, b3 being Real such that
A9: ( (b1 + b2) + b3 = 1 & x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ) by A8;
A10: x = (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + (b2 * (((a21 * y1) + (a22 * y2)) + (a23 * y3)))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3))) by A3, A5, A7, A9, Th27
.= (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + (b3 * (((a31 * y1) + (a32 * y2)) + (a33 * y3))) by Th27
.= (((((b1 * a11) * y1) + ((b1 * a12) * y2)) + ((b1 * a13) * y3)) + ((((b2 * a21) * y1) + ((b2 * a22) * y2)) + ((b2 * a23) * y3))) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3)) by Th27
.= (((((b1 * a11) + (b2 * a21)) * y1) + (((b1 * a12) + (b2 * a22)) * y2)) + (((b1 * a13) + (b2 * a23)) * y3)) + ((((b3 * a31) * y1) + ((b3 * a32) * y2)) + ((b3 * a33) * y3)) by Th29
.= (((((b1 * a11) + (b2 * a21)) + (b3 * a31)) * y1) + ((((b1 * a12) + (b2 * a22)) + (b3 * a32)) * y2)) + ((((b1 * a13) + (b2 * a23)) + (b3 * a33)) * y3) by Th29 ;
((((b1 * a11) + (b2 * a21)) + (b3 * a31)) + (((b1 * a12) + (b2 * a22)) + (b3 * a32))) + (((b1 * a13) + (b2 * a23)) + (b3 * a33)) = ((b1 * ((a11 + a12) + a13)) + (b2 * ((a21 + a22) + a23))) + (b3 * ((a31 + a32) + a33))
.= 1 by A3, A5, A7, A9 ;
hence x in plane y1,y2,y3 by A10; :: thesis: verum