let x, y, z be Element of (TOP-REAL 1); :: thesis: x,y,z are_collinear
per cases ( z <> y or z = y ) ;
suppose A1: z <> y ; :: thesis: x,y,z are_collinear
reconsider L = Line (y,z) as line of (TOP-REAL 1) ;
H1: ( y in L & z in L ) by RLTOPSP1:72;
reconsider x1 = x, y1 = y, z1 = z as Element of REAL 1 by EUCLID:22;
A2: ( x1 in REAL 1 & y1 in REAL 1 & z1 in REAL 1 ) ;
consider xr being Element of REAL such that
A3: x = <*xr*> by A2, FINSEQ_2:97;
consider yr being Element of REAL such that
A4: y = <*yr*> by A2, FINSEQ_2:97;
consider zr being Element of REAL such that
A5: z = <*zr*> by A2, FINSEQ_2:97;
A6: zr - yr <> 0 by A4, A5, A1;
reconsider r = (xr - yr) / (zr - yr) as Real ;
A7: ((1 - r) * yr) + (r * zr) = yr + (((xr - yr) / (zr - yr)) * (zr - yr))
.= yr + (xr - yr) by A6, XCMPLX_1:87
.= xr ;
((1 - r) * y1) + (r * z1) = <*((1 - r) * yr)*> + (r * <*zr*>) by A4, A5, RVSUM_1:47
.= <*((1 - r) * yr)*> + <*(r * zr)*> by RVSUM_1:47
.= x by RVSUM_1:13, A3, A7 ;
then x in { (((1 - r) * y1) + (r * z1)) where r is Real : verum } ;
then x in Line (y1,z1) by EUCLID_4:def 1;
then x in L by EUCLID12:4;
hence x,y,z are_collinear by H1; :: thesis: verum
end;
suppose z = y ; :: thesis: x,y,z are_collinear
then ( x in Line (x,y) & y in Line (x,y) & z in Line (x,y) ) by RLTOPSP1:72;
hence x,y,z are_collinear ; :: thesis: verum
end;
end;