let a, b, x be real number ; :: thesis: ( a <= x & x <= b implies (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace 0 ,1) )
assume A1: ( a <= x & x <= b ) ; :: thesis: (x - a) / (b - a) in the carrier of (Closed-Interval-TSpace 0 ,1)
then A2: x - a <= b - a by XREAL_1:11;
A3: a <= b by A1, XXREAL_0:2;
then A4: b - a >= 0 by XREAL_1:50;
A5: (x - a) / (b - a) <= 1

proof

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

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 A2, XREAL_1:187; :: thesis: verum

end;

end;

end;

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