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

proof

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

per cases ( y = 1 or y <> 1 ) ;

suppose y = 1 ; :: thesis: I_{-3} . (x1,y) >= I_{-3} . (x2,y)

then ( I_{-3} . (x1,y) = 1 & I_{-3} . (x2,y) = 1 ) by I3Def;
hence I_{-3} . (x1,y) >= I_{-3} . (x2,y) ; :: thesis: verum

end;

suppose y <> 1 ; :: thesis: I_{-3} . (x1,y) >= I_{-3} . (x2,y)

then y < 1 by SS, XXREAL_0:1;
then ( I_{-3} . (x1,y) = 0 & I_{-3} . (x2,y) = 0 ) by I3Def;
hence I_{-3} . (x1,y) >= I_{-3} . (x2,y) ; :: thesis: verum

end;

end;

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies I_{-3} . (x,y1) <= I_{-3} . (x,y2) )
assume YY: y1 <= y2 ; :: thesis: I_{-3} . (x,y1) <= I_{-3} . (x,y2)

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

suppose Y0: y1 = 1 ; :: thesis: I_{-3} . (x,y1) <= I_{-3} . (x,y2)

( y2 >= 1 & y2 <= 1 ) by XXREAL_1:1, Y0, YY;
then y2 = 1 by XXREAL_0:1;
then I_{-3} . (x,y2) = 1 by I3Def;
hence I_{-3} . (x,y1) <= I_{-3} . (x,y2) by XXREAL_1:1; :: thesis: verum

end;

suppose Za: ( y1 <> 1 & y2 = 1 ) ; :: thesis: I_{-3} . (x,y1) <= I_{-3} . (x,y2)

y1 <= 1 by XXREAL_1:1;
then y1 < 1 by Za, XXREAL_0:1;
then I_{-3} . (x,y1) = 0 by I3Def;
hence I_{-3} . (x,y1) <= I_{-3} . (x,y2) by Za, I3Def; :: thesis: verum

end;

suppose Za: ( y1 <> 1 & y2 <> 1 ) ; :: thesis: I_{-3} . (x,y1) <= I_{-3} . (x,y2)

( y1 <= 1 & y2 <= 1 ) by XXREAL_1:1;
then ( y1 < 1 & y2 < 1 ) by Za, XXREAL_0:1;
then ( I_{-3} . (x,y1) = 0 & I_{-3} . (x,y2) = 0 ) by I3Def;
hence I_{-3} . (x,y1) <= I_{-3} . (x,y2) ; :: thesis: verum

end;

end;

end;

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