let n be Nat; :: thesis: for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
Line (y1,y2) c= Line (x1,x2)
let y1, x1, x2, y2 be Element of REAL n; :: 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) ;

now

let z be set ; :: thesis: ( z in Line (y1,y2) implies 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, RVSUM_1:51
.= (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:51
.= ((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2)) by RVSUM_1:49
.= (((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by FINSEQOP:28
.= (((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by Lm2
.= ((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by FINSEQOP:28
.= ((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by RVSUM_1:50
.= ((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2) by RVSUM_1:50 ;
hence z in Line (x1,x2) ; :: thesis: verum

end;

hence Line (y1,y2) c= Line (x1,x2) by TARSKI:def 3; :: thesis: verum