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

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