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

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies I_I3 . (x1,y) >= I_I3 . (x2,y) )
assume Z1: x1 <= x2 ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

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

suppose Z0: x2 = 0 ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

then x1 = 0 by Z1, XXREAL_1:1;
hence I_I3 . (x1,y) >= I_I3 . (x2,y) by Z0; :: thesis: verum

end;

suppose ( x2 <> 0 & x1 <> 0 & y = 0 ) ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

then I_I3 . (x2,y) = 0 by II3Def;
hence I_I3 . (x1,y) >= I_I3 . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose ( x2 <> 0 & x1 <> 0 & y <> 0 ) ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

then ( I_I3 . (x1,y) = 1 & I_I3 . (x2,y) = 1 ) by II3Def;
hence I_I3 . (x1,y) >= I_I3 . (x2,y) ; :: thesis: verum

end;

suppose ( x2 <> 0 & x1 = 0 & y = 0 ) ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

then ( I_I3 . (x1,y) = 1 & I_I3 . (x2,y) = 0 ) by II3Def;
hence I_I3 . (x1,y) >= I_I3 . (x2,y) ; :: thesis: verum

end;

suppose Z1: ( x2 <> 0 & x1 = 0 & y <> 0 ) ; :: thesis: I_I3 . (x1,y) >= I_I3 . (x2,y)

then I_I3 . (x2,y) = 1 by II3Def;
hence I_I3 . (x1,y) >= I_I3 . (x2,y) by Z1, II3Def; :: thesis: verum

end;

end;

end;

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

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies I_I3 . (x,y1) <= I_I3 . (x,y2) )
assume SA: y1 <= y2 ; :: thesis: I_I3 . (x,y1) <= I_I3 . (x,y2)

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

suppose x = 0 ; :: thesis: I_I3 . (x,y1) <= I_I3 . (x,y2)

then ( I_I3 . (x,y1) = 1 & I_I3 . (x,y2) = 1 ) by II3Def;
hence I_I3 . (x,y1) <= I_I3 . (x,y2) ; :: thesis: verum

end;

suppose Z1: ( x <> 0 & y1 <> 0 ) ; :: thesis: I_I3 . (x,y1) <= I_I3 . (x,y2)

then y2 > 0 by SA, XXREAL_1:1;
then ( I_I3 . (x,y1) = 1 & I_I3 . (x,y2) = 1 ) by Z1, II3Def;
hence I_I3 . (x,y1) <= I_I3 . (x,y2) ; :: thesis: verum

end;

suppose ( x <> 0 & y1 = 0 & y2 = 0 ) ; :: thesis: I_I3 . (x,y1) <= I_I3 . (x,y2)

hence I_I3 . (x,y1) <= I_I3 . (x,y2) ; :: thesis: verum

end;

suppose ( x <> 0 & y1 = 0 & y2 <> 0 ) ; :: thesis: I_I3 . (x,y1) <= I_I3 . (x,y2)

then ( I_I3 . (x,y1) = 0 & I_I3 . (x,y2) = 1 ) by II3Def;
hence I_I3 . (x,y1) <= I_I3 . (x,y2) ; :: thesis: verum

end;

end;

end;

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