let a, b, x be Real; :: thesis: ( a <= x & x <= b implies (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1)) )
assume that
A1: a <= x and
A2: x <= b ; :: thesis: (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1))
A3: a <= b by A1, A2, XXREAL_0:2;
A4: x - a <= b - a by A2, XREAL_1:9;
A5: (x - a) / (b - a) <= 1

proof

per cases ( b - a = 0 or b - a > 0 ) by A3, XREAL_1:48;

suppose b - a = 0 ; :: thesis: (x - a) / (b - a) <= 1

hence (x - a) / (b - a) <= 1 by XCMPLX_1:49; :: thesis: verum

end;

suppose b - a > 0 ; :: thesis: (x - a) / (b - a) <= 1

hence (x - a) / (b - a) <= 1 by A4, XREAL_1:185; :: thesis: verum

end;

end;

end;

A6: x - a >= 0 by A1, XREAL_1:48;
b - a >= 0 by A3, XREAL_1:48;
then (x - a) / (b - a) in [.0,1.] by A5, A6, XXREAL_1:1;
hence (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18; :: thesis: verum