let n be Nat; :: thesis: for x1, x2, x3, y1, y2, y3 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, x2, x3, y1, y2, y3 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 that
A1: x1 in plane (y1,y2,y3) and
A2: x2 in plane (y1,y2,y3) and
A3: x3 in plane (y1,y2,y3) ; :: thesis: plane (x1,x2,x3) c= plane (y1,y2,y3)
ex x29 being Element of REAL n st
( x2 = x29 & ex a21, a22, a23 being Real st
( (a21 + a22) + a23 = 1 & x29 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ) ) by A2;
then consider a21, a22, a23 being Real such that
A4: (a21 + a22) + a23 = 1 and
A5: x2 = ((a21 * y1) + (a22 * y2)) + (a23 * y3) ;
ex x19 being Element of REAL n st
( x1 = x19 & ex a11, a12, a13 being Real st
( (a11 + a12) + a13 = 1 & x19 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ) ) by A1;
then consider a11, a12, a13 being Real such that
A6: (a11 + a12) + a13 = 1 and
A7: x1 = ((a11 * y1) + (a12 * y2)) + (a13 * y3) ;
let x be object ; :: 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 ex x9 being Element of REAL n st
( x = x9 & ex b1, b2, b3 being Real st
( (b1 + b2) + b3 = 1 & x9 = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ) ) ;
then consider b1, b2, b3 being Real such that
A8: (b1 + b2) + b3 = 1 and
A9: x = ((b1 * x1) + (b2 * x2)) + (b3 * x3) ;
ex x39 being Element of REAL n st
( x3 = x39 & ex a31, a32, a33 being Real st
( (a31 + a32) + a33 = 1 & x39 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ) ) by A3;
then consider a31, a32, a33 being Real such that
A10: (a31 + a32) + a33 = 1 and
A11: x3 = ((a31 * y1) + (a32 * y2)) + (a33 * y3) ;
A12: ((((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 A6, A4, A10, A8 ;
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 A7, A5, A11, A9, Th22
.= (((((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 Th22
.= (((((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 Th22
.= (((((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 Th24
.= (((((b1 * a11) + (b2 * a21)) + (b3 * a31)) * y1) + ((((b1 * a12) + (b2 * a22)) + (b3 * a32)) * y2)) + ((((b1 * a13) + (b2 * a23)) + (b3 * a33)) * y3) by Th24 ;
hence x in plane (y1,y2,y3) by A12; :: thesis: verum