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

proof

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

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

suppose Z0: x2 = 0 ; :: thesis: I_{-4} . (x1,y) >= I_{-4} . (x2,y)

then x1 = 0 by Z1, XXREAL_1:1;
hence I_{-4} . (x1,y) >= I_{-4} . (x2,y) by Z0; :: thesis: verum

end;

suppose ( x2 <> 0 & x1 <> 0 ) ; :: thesis: I_{-4} . (x1,y) >= I_{-4} . (x2,y)

then ( x1 > 0 & x2 > 0 ) by XXREAL_1:1;
then I_{-4} . (x2,y) = 0 by I4Def;
hence I_{-4} . (x1,y) >= I_{-4} . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose Z1: ( x2 <> 0 & x1 = 0 ) ; :: thesis: I_{-4} . (x1,y) >= I_{-4} . (x2,y)

x2 >= 0 by XXREAL_1:1;
then I_{-4} . (x2,y) = 0 by I4Def, Z1;
hence I_{-4} . (x1,y) >= I_{-4} . (x2,y) by Z1, I4Def; :: thesis: verum

end;

end;

end;

b2: for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
I_{-4} . (x,y1) <= I_{-4} . (x,y2)

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies I_{-4} . (x,y1) <= I_{-4} . (x,y2) )
SS: x >= 0 by XXREAL_1:1;
assume y1 <= y2 ; :: thesis: I_{-4} . (x,y1) <= I_{-4} . (x,y2)

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: I_{-4} . (x,y1) <= I_{-4} . (x,y2)

then ( I_{-4} . (x,y1) = 1 & I_{-4} . (x,y2) = 1 ) by I4Def;
hence I_{-4} . (x,y1) <= I_{-4} . (x,y2) ; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: I_{-4} . (x,y1) <= I_{-4} . (x,y2)

then ( I_{-4} . (x,y1) = 0 & I_{-4} . (x,y2) = 0 ) by I4Def, SS;
hence I_{-4} . (x,y1) <= I_{-4} . (x,y2) ; :: thesis: verum

end;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
hence ( I_{-4} is decreasing_on_1st & I_{-4} is increasing_on_2nd & I_{-4} is 00-dominant & not I_{-4} is 11-dominant & I_{-4} is 10-weak ) by b1, b2, I4Def; :: thesis: verum