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) holds
Line (y1,y2) c= Line (x1,x2)
let x1, x2, y1, y2 be Element of V; :: thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies Line (y1,y2) c= Line (x1,x2) )
assume y1 in Line (x1,x2) ; :: thesis: ( not y2 in Line (x1,x2) or Line (y1,y2) c= Line (x1,x2) )
then consider t being Real such that
A1: y1 = ((1 - t) * x1) + (t * x2) ;
assume y2 in Line (x1,x2) ; :: thesis: Line (y1,y2) c= Line (x1,x2)
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Line (y1,y2) or z in Line (x1,x2) )
assume z in Line (y1,y2) ; :: thesis: z in Line (x1,x2)
then consider u being Real such that
A3: z = ((1 - u) * y1) + (u * y2) ;
z = (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + (u * (((1 - s) * x1) + (s * x2))) by A1, A2, A3, RLVECT_1:def 5
.= (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RLVECT_1:def 5
.= ((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RLVECT_1:def 7
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RLVECT_1:def 7
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2))) by RLVECT_1:def 7
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2)) by RLVECT_1:def 7
.= (((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by RLVECT_1:def 3
.= (((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by RLVECT_1:def 3
.= ((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by RLVECT_1:def 3
.= ((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by RLVECT_1:def 6
.= ((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2) by RLVECT_1:def 6 ;
hence z in Line (x1,x2) ; :: thesis: verum