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:73
.= (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:73
.= ((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:71
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:71
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2))) by RVSUM_1:71
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2)) by RVSUM_1:71
.= (((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by FINSEQOP:29
.= (((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:29
.= ((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by RVSUM_1:72
.= ((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2) by RVSUM_1:72 ;
hence z in Line x1,x2 ; :: thesis: verum

end;

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