let x, y be Element of [.0,1.]; :: thesis: (x * y) + ((1 - x) * 1) in [.y,1.]
( 0 <= x & x <= 1 & y <= 1 ) by XXREAL_1:1;
then A1: y <= ((1 - x) * 1) + (x * y) by XREAL_1:173;
( 0 <= x & x <= 1 & y <= 1 ) by XXREAL_1:1;
then ((1 - x) * 1) + (x * y) <= 1 by XREAL_1:174;
hence (x * y) + ((1 - x) * 1) in [.y,1.] by A1, XXREAL_1:1; :: thesis: verum