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)

proof

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)

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

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

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

end;

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

( x1 >= 0 & y <= 1 ) by XXREAL_1:1;
then W2: ( x1 > 0 & y < 1 ) by W1, XXREAL_0:1;
then I_{0} . (x1,y) = 0 by I0Impl;
hence I_{0} . (x1,y) >= I_{0} . (x2,y) by I0Impl, W2, W0; :: thesis: verum

end;

end;

end;

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

proof

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)

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

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;

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;

end;

end;

( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
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