let n be Element of NAT ; :: thesis: for y1, x1, x2, x3, 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 y1, x1, x2, x3, 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 set ; :: 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, Th27
.= (((((1 - t) * a11) * x1) + (((1 - t) * a12) * x2)) + (((1 - t) * a13) * x3)) + ((((t * a21) * x1) + ((t * a22) * x2)) + ((t * a23) * x3)) by Th27
.= (((((1 - t) * a11) + (t * a21)) * x1) + ((((1 - t) * a12) + (t * a22)) * x2)) + ((((1 - t) * a13) + (t * a23)) * x3) by Th29 ;
hence x in plane x1,x2,x3 by A12; :: thesis: verum

end;

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