for a, b, x being Real st a <= x & x <= b holds
(x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1))