let a, b, c be Element of RealSpace; :: thesis: ( b in [.a,c.] implies b is_Between a,c )
assume b in [.a,c.] ; :: thesis: b is_Between a,c
then B1: ( b >= a + 0 & c >= b + 0 ) by XXREAL_1:1;
then b2: c >= a + 0 by XXREAL_0:2;
A0: |.(a - c).| = |.(c - a).| by COMPLEX1:60
.= (c - b) + (b - a) by b2, COMPLEX1:43, XREAL_1:19
.= |.(c - b).| + (b - a) by B1, XREAL_1:19, COMPLEX1:43
.= |.(c - b).| + |.(b - a).| by B1, XREAL_1:19, COMPLEX1:43
.= |.(b - c).| + |.(b - a).| by COMPLEX1:60
.= |.(a - b).| + |.(b - c).| by COMPLEX1:60 ;
A1: dist (a,c) = |.(a - c).| by TOPMETR:11;
dist (a,b) = |.(a - b).| by TOPMETR:11;
hence b is_Between a,c by A1, A0, TOPMETR:11; :: thesis: verum