let M be non empty trivial MetrSpace; :: thesis: for a, b, c being Element of M holds a is_Between b,c
let a, b, c be Element of M; :: thesis: a is_Between b,c
( a = b & b = c ) by STRUCT_0:def 10;
then ( dist (b,a) = 0 & dist (a,c) = 0 & dist (b,c) = 0 ) by METRIC_1:1;
then a is_Between b,c ;
hence a is_Between b,c ; :: thesis: verum