let V be RealLinearSpace; :: thesis: for x1, x2, y1, y2 being Element of V st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (y1,y2) = Line (x1,x2)
let x1, x2, y1, y2 be Element of V; :: thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 implies Line (y1,y2) = Line (x1,x2) )
assume A1: y1 in Line (x1,x2) ; :: thesis: ( not y2 in Line (x1,x2) or not y1 <> y2 or Line (y1,y2) = Line (x1,x2) )
then consider t being Real such that
A2: y1 = ((1 - t) * x1) + (t * x2) ;
assume A3: y2 in Line (x1,x2) ; :: thesis: ( not y1 <> y2 or Line (y1,y2) = Line (x1,x2) )
then consider s being Real such that
A4: y2 = ((1 - s) * x1) + (s * x2) ;
assume y1 <> y2 ; :: thesis: Line (y1,y2) = Line (x1,x2)
then A5: t - s <> 0 by A2, A4;
thus Line (y1,y2) c= Line (x1,x2) by A1, A3, Th74; :: according to XBOOLE_0:def 10 :: thesis: Line (x1,x2) c= Line (y1,y2)
((1 - ((t - 1) / (t - s))) * y1) + (((t - 1) / (t - s)) * y2) = ((((1 * (t - s)) - (t - 1)) / (t - s)) * y1) + (((t - 1) / (t - s)) * y2) by A5, XCMPLX_1:127
.= (((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + (((t - 1) / (t - s)) * (((1 - s) * x1) + (s * x2))) by A2, A4, RLVECT_1:def 5
.= (((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RLVECT_1:def 5
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + (((t - 1) / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by RLVECT_1:def 7
.= (((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2))) by RLVECT_1:def 3
.= (((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by RLVECT_1:def 3
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((t - 1) * (1 - s)) / (t - s)) * x1)) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)) by RLVECT_1:def 3
.= ((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)) by RLVECT_1:def 6
.= ((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2) by RLVECT_1:def 6
.= (0. V) + ((((((- s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2) by RLVECT_1:10
.= ((1 * (t - s)) / (t - s)) * x2
.= 1 * x2 by A5, XCMPLX_1:89
.= x2 by RLVECT_1:def 8 ;
then A6: x2 in Line (y1,y2) ;
((1 - (t / (t - s))) * y1) + ((t / (t - s)) * y2) = ((((1 * (t - s)) - t) / (t - s)) * y1) + ((t / (t - s)) * y2) by A5, XCMPLX_1:127
.= ((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + ((t / (t - s)) * (((1 - s) * x1) + (s * x2))) by A2, A4, RLVECT_1:def 5
.= ((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RLVECT_1:def 5
.= (((((- s) / (t - s)) * (1 - t)) * x1) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + ((t / (t - s)) * (s * x2))) by RLVECT_1:def 7
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by RLVECT_1:def 7
.= ((((- s) * (1 - t)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2))) by RLVECT_1:def 3
.= ((((- s) * (1 - t)) / (t - s)) * x1) + ((((t * (1 - s)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by RLVECT_1:def 3
.= (((((- s) * (1 - t)) / (t - s)) * x1) + (((t * (1 - s)) / (t - s)) * x1)) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)) by RLVECT_1:def 3
.= (((((- s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)) by RLVECT_1:def 6
.= (((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (((((- s) * t) / (t - s)) + ((t * s) / (t - s))) * x2) by RLVECT_1:def 6
.= (((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (0. V) by RLVECT_1:10
.= ((1 * (t - s)) / (t - s)) * x1
.= 1 * x1 by A5, XCMPLX_1:89
.= x1 by RLVECT_1:def 8 ;
then x1 in Line (y1,y2) ;
hence Line (x1,x2) c= Line (y1,y2) by A6, Th74; :: thesis: verum