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

( 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