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

proof

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

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

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

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

end;

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

x2 <= 1 by XXREAL_1:1;
then Y3: x2 < 1 by W1, XXREAL_0:1;
then Y2: I_{1} . (x2,y) = 1 by I1Impl;
x1 < 1 by XXREAL_0:2, A0, Y3;
hence I_{1} . (x1,y) >= I_{1} . (x2,y) by Y2, I1Impl; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

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

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

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

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

end;

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

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

end;

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

x <= 1 by XXREAL_1:1;
then A2: x < 1 by B1, XXREAL_0:1;
then I_{1} . (x,y1) = 1 by I1Impl;
hence I_{1} . (x,y1) <= I_{1} . (x,y2) by A2, I1Impl; :: thesis: verum

end;

end;

end;

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