let S be TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st ( Middle a,b,c or between a,b,c ) holds
Collinear a,b,c
let a, b, c be POINT of S; :: thesis: ( ( Middle a,b,c or between a,b,c ) implies Collinear a,b,c )
assume ( Middle a,b,c or between a,b,c ) ; :: thesis: Collinear a,b,c
then between a,b,c by GTARSKI3:def 12;
hence Collinear a,b,c by GTARSKI1:def 17; :: thesis: verum