set I = I_FD ;
A1: I_FD is satisfying_(OP)

proof

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 )

proof

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;

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

end;

for x, y, z being Element of [.0,1.] holds I_FD . (x,(I_FD . (y,z))) = I_FD . (y,(I_FD . (x,z)))

proof

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;

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

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;

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;

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;

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

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;

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;

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;

end;

end;

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;

end;

end;

then I_FD is satisfying_(EP) ;
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