theorem :: GTARSKI1:47

for a, b, c being Element of RealSpace st b in [.a,c.] holds
b is_Between a,c