let a be Element of [.0,1.]; :: thesis: 1 - a in [.0,1.]
( 0 <= a & a <= 1 ) by XXREAL_1:1;
then ( 1 - 1 <= 1 - a & 1 - a <= 1 - 0 ) by XREAL_1:13;
hence 1 - a in [.0,1.] by XXREAL_1:1; :: thesis: verum