set f = I_{-2} ;
b1:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
I_{-2} . (x1,y) >= I_{-2} . (x2,y)
proof
let x1,
x2,
y be
Element of
[.0,1.];
( x1 <= x2 implies I_{-2} . (x1,y) >= I_{-2} . (x2,y) )
assume Z1:
x1 <= x2
;
I_{-2} . (x1,y) >= I_{-2} . (x2,y)
Z2:
(
I_{-2} . (
x1,
y)
= max (
y,
(min ((1 - x1),(1 - y)))) &
I_{-2} . (
x2,
y)
= max (
y,
(min ((1 - x2),(1 - y)))) )
by I2Def;
1
- x1 >= 1
- x2
by Z1, XREAL_1:13;
then
min (
(1 - x1),
(1 - y))
>= min (
(1 - x2),
(1 - y))
by XXREAL_0:18;
hence
I_{-2} . (
x1,
y)
>= I_{-2} . (
x2,
y)
by Z2, XXREAL_0:26;
verum
end;
S:
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
then T1: I_{-2} . (0,0) =
max (0,(min ((1 - 0),(1 - 0))))
by I2Def
.=
1
by XXREAL_0:def 10
;
T2: I_{-2} . (1,0) =
max (0,(min ((1 - 1),(1 - 0))))
by S, I2Def
.=
max (0,0)
by XXREAL_0:def 9
.=
0
;
I_{-2} . (1,1) =
max (1,(min ((1 - 1),(1 - 1))))
by S, I2Def
.=
1
by XXREAL_0:def 10
;
hence
( I_{-2} is decreasing_on_1st & I_{-2} is 00-dominant & I_{-2} is 11-dominant & I_{-2} is 10-weak )
by b1, T1, T2; verum