let a, b, c be Element of RealSpace; ( b in [.a,c.] implies b is_Between a,c )
assume
b in [.a,c.]
; 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; verum