set f = I_{-2} ;

b1: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

I_{-2} . (x1,y) >= I_{-2} . (x2,y)

then T1: I_{-2} . (0,0) = max (0,(min ((1 - 0),(1 - 0)))) by I2Def

.= 1 by XXREAL_0:def 10 ;

T2: I_{-2} . (1,0) = max (0,(min ((1 - 1),(1 - 0)))) by S, I2Def

.= max (0,0) by XXREAL_0:def 9

.= 0 ;

I_{-2} . (1,1) = max (1,(min ((1 - 1),(1 - 1)))) by S, I2Def

.= 1 by XXREAL_0:def 10 ;

hence ( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak ) by b1, T1, T2; :: thesis: verum

b1: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds

I_{-2} . (x1,y) >= I_{-2} . (x2,y)

proof

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

assume Z1: x1 <= x2 ; :: thesis: I_{-2} . (x1,y) >= I_{-2} . (x2,y)

Z2: ( I_{-2} . (x1,y) = max (y,(min ((1 - x1),(1 - y)))) & I_{-2} . (x2,y) = max (y,(min ((1 - x2),(1 - y)))) ) by I2Def;

1 - x1 >= 1 - x2 by Z1, XREAL_1:13;

then min ((1 - x1),(1 - y)) >= min ((1 - x2),(1 - y)) by XXREAL_0:18;

hence I_{-2} . (x1,y) >= I_{-2} . (x2,y) by Z2, XXREAL_0:26; :: thesis: verum

end;assume Z1: x1 <= x2 ; :: thesis: I_{-2} . (x1,y) >= I_{-2} . (x2,y)

Z2: ( I_{-2} . (x1,y) = max (y,(min ((1 - x1),(1 - y)))) & I_{-2} . (x2,y) = max (y,(min ((1 - x2),(1 - y)))) ) by I2Def;

1 - x1 >= 1 - x2 by Z1, XREAL_1:13;

then min ((1 - x1),(1 - y)) >= min ((1 - x2),(1 - y)) by XXREAL_0:18;

hence I_{-2} . (x1,y) >= I_{-2} . (x2,y) by Z2, XXREAL_0:26; :: thesis: verum

then T1: I_{-2} . (0,0) = max (0,(min ((1 - 0),(1 - 0)))) by I2Def

.= 1 by XXREAL_0:def 10 ;

T2: I_{-2} . (1,0) = max (0,(min ((1 - 1),(1 - 0)))) by S, I2Def

.= max (0,0) by XXREAL_0:def 9

.= 0 ;

I_{-2} . (1,1) = max (1,(min ((1 - 1),(1 - 1)))) by S, I2Def

.= 1 by XXREAL_0:def 10 ;

hence ( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak ) by b1, T1, T2; :: thesis: verum