let n be Nat; 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; ( 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)
; 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 ; TARSKI:def 3 ( not x in plane (x1,x2,x3) or x in plane (y1,y2,y3) )
assume
x in plane (x1,x2,x3)
; 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; verum