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

end;

end;

end;

A6: x - a >= 0 by A1, XREAL_1:50;
b - a >= 0 by A3, XREAL_1:50;
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:25; :: thesis: verum