let n be Nat; for x1, x2, x3, y1, y2 being Element of REAL n st y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) holds
Line (y1,y2) c= plane (x1,x2,x3)
let x1, x2, x3, y1, y2 be Element of REAL n; ( y1 in plane (x1,x2,x3) & y2 in plane (x1,x2,x3) implies Line (y1,y2) c= plane (x1,x2,x3) )
assume that
A1:
y1 in plane (x1,x2,x3)
and
A2:
y2 in plane (x1,x2,x3)
; Line (y1,y2) c= plane (x1,x2,x3)
consider y29 being Element of REAL n such that
A3:
y2 = y29
and
A4:
ex a21, a22, a23 being Real st
( (a21 + a22) + a23 = 1 & y29 = ((a21 * x1) + (a22 * x2)) + (a23 * x3) )
by A2;
consider y19 being Element of REAL n such that
A5:
y1 = y19
and
A6:
ex a11, a12, a13 being Real st
( (a11 + a12) + a13 = 1 & y19 = ((a11 * x1) + (a12 * x2)) + (a13 * x3) )
by A1;
Line (y1,y2) c= plane (x1,x2,x3)
proof
let x be
object ;
TARSKI:def 3 ( not x in Line (y1,y2) or x in plane (x1,x2,x3) )
assume
x in Line (
y1,
y2)
;
x in plane (x1,x2,x3)
then consider t being
Real such that A7:
x = ((1 - t) * y1) + (t * y2)
;
consider a21,
a22,
a23 being
Real such that A8:
(a21 + a22) + a23 = 1
and A9:
y29 = ((a21 * x1) + (a22 * x2)) + (a23 * x3)
by A4;
consider a11,
a12,
a13 being
Real such that A10:
(a11 + a12) + a13 = 1
and A11:
y19 = ((a11 * x1) + (a12 * x2)) + (a13 * x3)
by A6;
A12:
((((1 - t) * a11) + (t * a21)) + (((1 - t) * a12) + (t * a22))) + (((1 - t) * a13) + (t * a23)) =
((1 - t) * ((a11 + a12) + a13)) + (t * ((a21 + a22) + a23))
.=
(1 - t) + t
by A10, A8
.=
1
;
x =
(((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + (t * (((a21 * x1) + (a22 * x2)) + (a23 * x3)))
by A5, A3, A7, A11, A9, Th22
.=
(((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + ((((t * a21) * x1) + ((t * a22) * x2)) + ((t * a23) * x3))
by Th22
.=
(((((1 - t) * a11) + (t * a21)) * x1) + ((((1 - t) * a12) + (t * a22)) * x2)) + ((((1 - t) * a13) + (t * a23)) * x3)
by Th24
;
hence
x in plane (
x1,
x2,
x3)
by A12;
verum
end;
hence
Line (y1,y2) c= plane (x1,x2,x3)
; verum