set f = I_{0} ;

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

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

I_{0} . (x,y1) <= I_{0} . (x,y2)

hence ( I_{0} is decreasing_on_1st & I_{0} is increasing_on_2nd & I_{0} is 00-dominant & I_{0} is 11-dominant & I_{0} is 10-weak ) by b1, b2, I0Impl; :: thesis: verum

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

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

proof

b2:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies I_{0} . (x1,y) >= I_{0} . (x2,y) )

assume W0: x1 <= x2 ; :: thesis: I_{0} . (x1,y) >= I_{0} . (x2,y)

end;assume W0: x1 <= x2 ; :: thesis: I_{0} . (x1,y) >= I_{0} . (x2,y)

I_{0} . (x,y1) <= I_{0} . (x,y2)

proof

( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies I_{0} . (x,y1) <= I_{0} . (x,y2) )

assume WW: y1 <= y2 ; :: thesis: I_{0} . (x,y1) <= I_{0} . (x,y2)

end;assume WW: y1 <= y2 ; :: thesis: I_{0} . (x,y1) <= I_{0} . (x,y2)

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

end;

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

then
I_{0} . (x,y2) = 1
by I0Impl;

hence I_{0} . (x,y1) <= I_{0} . (x,y2) by XXREAL_1:1; :: thesis: verum

end;hence I_{0} . (x,y1) <= I_{0} . (x,y2) by XXREAL_1:1; :: thesis: verum

suppose Ww:
( y2 <> 1 & x <> 0 )
; :: thesis: I_{0} . (x,y1) <= I_{0} . (x,y2)

wc:
( y2 <= 1 & x >= 0 )
by XXREAL_1:1;

then Wc: ( y2 < 1 & x > 0 ) by Ww, XXREAL_0:1;

then Wd: I_{0} . (x,y2) = 0 by I0Impl;

y1 < 1 by WW, Wc, XXREAL_0:2;

hence I_{0} . (x,y1) <= I_{0} . (x,y2) by Wd, wc, I0Impl, Ww; :: thesis: verum

end;then Wc: ( y2 < 1 & x > 0 ) by Ww, XXREAL_0:1;

then Wd: I_{0} . (x,y2) = 0 by I0Impl;

y1 < 1 by WW, Wc, XXREAL_0:2;

hence I_{0} . (x,y1) <= I_{0} . (x,y2) by Wd, wc, I0Impl, Ww; :: thesis: verum

hence ( I_{0} is decreasing_on_1st & I_{0} is increasing_on_2nd & I_{0} is 00-dominant & I_{0} is 11-dominant & I_{0} is 10-weak ) by b1, b2, I0Impl; :: thesis: verum