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

end;

hence Line (y1,y2) c= plane (x1,x2,x3) ; :: thesis: verum