set f = I_I4 ;
b1: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
I_I4 . (x1,y) >= I_I4 . (x2,y)

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies I_I4 . (x1,y) >= I_I4 . (x2,y) )
assume Z1: x1 <= x2 ; :: thesis: I_I4 . (x1,y) >= I_I4 . (x2,y)

per cases ( x2 = 0 or y = 1 or x1 <> 1 or ( x1 = 1 & y <> 1 ) ) ;

suppose Z0: x2 = 0 ; :: thesis: I_I4 . (x1,y) >= I_I4 . (x2,y)

then x1 = 0 by Z1, XXREAL_1:1;
hence I_I4 . (x1,y) >= I_I4 . (x2,y) by Z0; :: thesis: verum

end;

suppose y = 1 ; :: thesis: I_I4 . (x1,y) >= I_I4 . (x2,y)

then ( I_I4 . (x1,y) = 1 & I_I4 . (x2,y) = 1 ) by II4Def;
hence I_I4 . (x1,y) >= I_I4 . (x2,y) ; :: thesis: verum

end;

suppose x1 <> 1 ; :: thesis: I_I4 . (x1,y) >= I_I4 . (x2,y)

then I_I4 . (x1,y) = 1 by II4Def;
hence I_I4 . (x1,y) >= I_I4 . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose I1: ( x1 = 1 & y <> 1 ) ; :: thesis: I_I4 . (x1,y) >= I_I4 . (x2,y)

x2 <= 1 by XXREAL_1:1;
hence I_I4 . (x1,y) >= I_I4 . (x2,y) by Z1, I1, XXREAL_0:1; :: thesis: verum

end;

end;

end;

b2: for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
I_I4 . (x,y1) <= I_I4 . (x,y2)

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies I_I4 . (x,y1) <= I_I4 . (x,y2) )
assume SA: y1 <= y2 ; :: thesis: I_I4 . (x,y1) <= I_I4 . (x,y2)

per cases ( x <> 1 or y1 = 1 or ( x = 1 & y1 <> 1 & y2 <> 1 ) or ( x = 1 & y1 <> 1 & y2 = 1 ) ) ;

suppose x <> 1 ; :: thesis: I_I4 . (x,y1) <= I_I4 . (x,y2)

then ( I_I4 . (x,y1) = 1 & I_I4 . (x,y2) = 1 ) by II4Def;
hence I_I4 . (x,y1) <= I_I4 . (x,y2) ; :: thesis: verum

end;

suppose Z1: y1 = 1 ; :: thesis: I_I4 . (x,y1) <= I_I4 . (x,y2)

then ( y2 >= 1 & y2 <= 1 ) by SA, XXREAL_1:1;
hence I_I4 . (x,y1) <= I_I4 . (x,y2) by Z1, XXREAL_0:1; :: thesis: verum

end;

suppose ( x = 1 & y1 <> 1 & y2 <> 1 ) ; :: thesis: I_I4 . (x,y1) <= I_I4 . (x,y2)

then ( I_I4 . (x,y1) = 0 & I_I4 . (x,y2) = 0 ) by II4Def;
hence I_I4 . (x,y1) <= I_I4 . (x,y2) ; :: thesis: verum

end;

suppose ( x = 1 & y1 <> 1 & y2 = 1 ) ; :: thesis: I_I4 . (x,y1) <= I_I4 . (x,y2)

then ( I_I4 . (x,y1) = 0 & I_I4 . (x,y2) = 1 ) by II4Def;
hence I_I4 . (x,y1) <= I_I4 . (x,y2) ; :: thesis: verum

end;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
hence ( I_I4 is decreasing_on_1st & I_I4 is increasing_on_2nd & I_I4 is 00-dominant & I_I4 is 11-dominant & I_I4 is 10-weak ) by b1, b2, II4Def; :: thesis: verum