set f = I_{-5} ;
b1:
for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
I_{-5} . (x1,y) >= I_{-5} . (x2,y)
proof
let x1,
x2,
y be
Element of
[.0,1.];
( x1 <= x2 implies I_{-5} . (x1,y) >= I_{-5} . (x2,y) )
assume
x1 <= x2
;
I_{-5} . (x1,y) >= I_{-5} . (x2,y)
(
I_{-5} . (
x1,
y)
= 1 &
I_{-5} . (
x2,
y)
= 1 )
by I5Def;
hence
I_{-5} . (
x1,
y)
>= I_{-5} . (
x2,
y)
;
verum
end;
b2:
for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
I_{-5} . (x,y1) <= I_{-5} . (x,y2)
proof
let x,
y1,
y2 be
Element of
[.0,1.];
( y1 <= y2 implies I_{-5} . (x,y1) <= I_{-5} . (x,y2) )
assume
y1 <= y2
;
I_{-5} . (x,y1) <= I_{-5} . (x,y2)
(
I_{-5} . (
x,
y1)
= 1 &
I_{-5} . (
x,
y2)
= 1 )
by I5Def;
hence
I_{-5} . (
x,
y1)
<= I_{-5} . (
x,
y2)
;
verum
end;
( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;
hence
( I_{-5} is decreasing_on_1st & I_{-5} is increasing_on_2nd & I_{-5} is 00-dominant & I_{-5} is 11-dominant & not I_{-5} is 10-weak )
by b1, b2, I5Def; verum