let M be non empty trivial MetrSpace; for a, b, c being Element of M holds a is_Between b,c
let a, b, c be Element of M; 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
; verum