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

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