set I = I_FD ;

A1: I_FD is satisfying_(OP)

hence ( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) ) by A1; :: thesis: verum

A1: I_FD is satisfying_(OP)

proof

for x, y, z being Element of [.0,1.] holds I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))
let x, y be Element of [.0,1.]; :: according to FUZIMPL2:def 4 :: thesis: ( I_FD . (x,y) = 1 iff x <= y )

thus ( I_FD . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_FD . (x,y) = 1 )

end;thus ( I_FD . (x,y) = 1 implies x <= y ) :: thesis: ( x <= y implies I_FD . (x,y) = 1 )

proof

thus
( x <= y implies I_FD . (x,y) = 1 )
by FUZIMPL1:def 23; :: thesis: verum
assume T2:
I_FD . (x,y) = 1
; :: thesis: x <= y

assume T3: x > y ; :: thesis: contradiction

then I_FD . (x,y) = max ((1 - x),y) by FUZIMPL1:def 23;

then ( 1 - x = 1 or y = 1 ) by XXREAL_0:16, T2;

hence contradiction by T3, XXREAL_1:1; :: thesis: verum

end;assume T3: x > y ; :: thesis: contradiction

then I_FD . (x,y) = max ((1 - x),y) by FUZIMPL1:def 23;

then ( 1 - x = 1 or y = 1 ) by XXREAL_0:16, T2;

hence contradiction by T3, XXREAL_1:1; :: thesis: verum

proof

then
I_FD is satisfying_(EP)
;
let x, y, z be Element of [.0,1.]; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

Ff: 1 in [.0,1.] by XXREAL_1:1;

F0: ( x <= 1 & y <= 1 & z >= 0 ) by XXREAL_1:1;

end;Ff: 1 in [.0,1.] by XXREAL_1:1;

F0: ( x <= 1 & y <= 1 & z >= 0 ) by XXREAL_1:1;

per cases
( ( y <= z & x <= z ) or ( y <= z & x > z ) or ( y > z & x > z ) or ( y > z & x <= z ) )
;

end;

suppose F1:
( y <= z & x <= z )
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

then F2: I_FD . (x,(I_FD . (y,z))) =
I_FD . (x,1)
by FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum

end;.= 1 by A1, F0, Ff ;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum

suppose F1:
( y <= z & x > z )
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

ff:
z <= max ((1 - x),z)
by XXREAL_0:25;

f4: I_FD . (x,z) = max ((1 - x),z) by FUZIMPL1:def 23, F1;

I_FD . (x,(I_FD . (y,z))) = I_FD . (x,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by A1, ff, F1, XXREAL_0:2, f4; :: thesis: verum

end;f4: I_FD . (x,z) = max ((1 - x),z) by FUZIMPL1:def 23, F1;

I_FD . (x,(I_FD . (y,z))) = I_FD . (x,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by A1, ff, F1, XXREAL_0:2, f4; :: thesis: verum

suppose F1:
( y > z & x > z )
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

x2:
I_FD . (y,z) = max ((1 - y),z)
by F1, FUZIMPL1:def 23;

x4: I_FD . (x,z) = max ((1 - x),z) by F1, FUZIMPL1:def 23;

end;x4: I_FD . (x,z) = max ((1 - x),z) by F1, FUZIMPL1:def 23;

per cases
( x <= max ((1 - y),z) or 1 - x < y or 1 - x >= y )
;

end;

suppose X1:
x <= max ((1 - y),z)
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

then
( x <= 1 - y or x <= z )
by XXREAL_0:def 10;

then x + y <= (1 - y) + y by XREAL_1:6, F1;

then y1: (x + y) - x <= 1 - x by XREAL_1:9;

1 - x <= max ((1 - x),z) by XXREAL_0:25;

then X3: y <= max ((1 - x),z) by y1, XXREAL_0:2;

I_FD . (x,(I_FD . (y,z))) = 1 by X1, x2, FUZIMPL1:def 23;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by X3, x4, FUZIMPL1:def 23; :: thesis: verum

end;then x + y <= (1 - y) + y by XREAL_1:6, F1;

then y1: (x + y) - x <= 1 - x by XREAL_1:9;

1 - x <= max ((1 - x),z) by XXREAL_0:25;

then X3: y <= max ((1 - x),z) by y1, XXREAL_0:2;

I_FD . (x,(I_FD . (y,z))) = 1 by X1, x2, FUZIMPL1:def 23;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by X3, x4, FUZIMPL1:def 23; :: thesis: verum

suppose we:
1 - x < y
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

then X3:
y > max ((1 - x),z)
by XXREAL_0:29, F1;

(1 - x) - y < y - y by we, XREAL_1:9;

then ((1 - x) - y) + x < 0 + x by XREAL_1:6;

then X1: x > max ((1 - y),z) by XXREAL_0:def 10, F1;

F2: I_FD . (x,(I_FD . (y,z))) = max ((1 - x),(max ((1 - y),z))) by x2, FUZIMPL1:def 23, X1;

I_FD . (y,(I_FD . (x,z))) = max ((1 - y),(max ((1 - x),z))) by FUZIMPL1:def 23, X3, x4;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2, XXREAL_0:34; :: thesis: verum

end;(1 - x) - y < y - y by we, XREAL_1:9;

then ((1 - x) - y) + x < 0 + x by XREAL_1:6;

then X1: x > max ((1 - y),z) by XXREAL_0:def 10, F1;

F2: I_FD . (x,(I_FD . (y,z))) = max ((1 - x),(max ((1 - y),z))) by x2, FUZIMPL1:def 23, X1;

I_FD . (y,(I_FD . (x,z))) = max ((1 - y),(max ((1 - x),z))) by FUZIMPL1:def 23, X3, x4;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2, XXREAL_0:34; :: thesis: verum

suppose SE:
1 - x >= y
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

then
(1 - x) + x >= y + x
by XREAL_1:6;

then ww: 1 - y >= (y + x) - y by XREAL_1:9;

then SA: max ((1 - y),z) = 1 - y by XXREAL_0:def 10, XXREAL_0:2, F1;

P0: ( 1 - x in [.0,1.] & 1 - y in [.0,1.] ) by FUZNORM1:7;

F2: I_FD . (x,(I_FD . (y,z))) = I_FD . (x,(max ((1 - y),z))) by F1, FUZIMPL1:def 23

.= 1 by P0, FUZIMPL1:def 23, ww, SA ;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,(max ((1 - x),z))) by F1, FUZIMPL1:def 23

.= I_FD . (y,(1 - x)) by SE, F1, XXREAL_0:2, XXREAL_0:def 10

.= 1 by A1, P0, SE ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum

end;then ww: 1 - y >= (y + x) - y by XREAL_1:9;

then SA: max ((1 - y),z) = 1 - y by XXREAL_0:def 10, XXREAL_0:2, F1;

P0: ( 1 - x in [.0,1.] & 1 - y in [.0,1.] ) by FUZNORM1:7;

F2: I_FD . (x,(I_FD . (y,z))) = I_FD . (x,(max ((1 - y),z))) by F1, FUZIMPL1:def 23

.= 1 by P0, FUZIMPL1:def 23, ww, SA ;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,(max ((1 - x),z))) by F1, FUZIMPL1:def 23

.= I_FD . (y,(1 - x)) by SE, F1, XXREAL_0:2, XXREAL_0:def 10

.= 1 by A1, P0, SE ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by F2; :: thesis: verum

suppose F1:
( y > z & x <= z )
; :: thesis: I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

f3:
z <= max ((1 - y),z)
by XXREAL_0:25;

f4: I_FD . (y,z) = max ((1 - y),z) by FUZIMPL1:def 23, F1;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by f4, A1, F1, f3, XXREAL_0:2; :: thesis: verum

end;f4: I_FD . (y,z) = max ((1 - y),z) by FUZIMPL1:def 23, F1;

I_FD . (y,(I_FD . (x,z))) = I_FD . (y,1) by F1, FUZIMPL1:def 23

.= 1 by A1, F0, Ff ;

hence I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z))) by f4, A1, F1, f3, XXREAL_0:2; :: thesis: verum

hence ( I_FD is satisfying_(NP) & I_FD is satisfying_(EP) & I_FD is satisfying_(IP) & I_FD is satisfying_(OP) ) by A1; :: thesis: verum