set f = I_{-1} ;
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 y1 <= y2 ; :: thesis: I_{-1} . (x,y1) <= I_{-1} . (x,y2)
then y1: min (x,y1) <= min (x,y2) by XXREAL_0:18;
( I_{-1} . (x,y1) = max ((1 - x),(min (x,y1))) & I_{-1} . (x,y2) = max ((1 - x),(min (x,y2))) ) by I1Def;
hence I_{-1} . (x,y1) <= I_{-1} . (x,y2) by y1, XXREAL_0:26; :: thesis: verum

end;

S: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
then T1: I_{-1} . (0,0) = max ((1 - 0),(min (0,0))) by I1Def
.= 1 by XXREAL_0:def 10 ;
T2: I_{-1} . (1,0) = max ((1 - 1),(min (1,0))) by S, I1Def
.= max (0,0) by XXREAL_0:def 9
.= 0 ;
I_{-1} . (1,1) = max ((1 - 1),(min (1,1))) by S, I1Def
.= 1 by XXREAL_0:def 10 ;
hence ( I_{-1} is increasing_on_2nd & I_{-1} is 00-dominant & I_{-1} is 11-dominant & I_{-1} is 10-weak ) by b2, T1, T2; :: thesis: verum