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.];
( y1 <= y2 implies I_{-1} . (x,y1) <= I_{-1} . (x,y2) )
assume
y1 <= y2
;
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;
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; verum