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

proof

let x, y be Element of [.0,1.]; :: according to FUZIMPL2:def 4 :: thesis: ( I_LK . (x,y) = 1 iff x <= y )
( I_LK . (x,y) = 1 implies x <= y )

proof

assume I_LK . (x,y) = 1 ; :: thesis: x <= y
then min (1,((1 - x) + y)) = 1 by FUZIMPL1:def 14;
then ((1 - x) + y) - 1 >= 1 - 1 by XREAL_1:9, XXREAL_0:def 9;
then (y - x) + x >= 0 + x by XREAL_1:6;
hence x <= y ; :: thesis: verum

end;

hence ( I_LK . (x,y) = 1 iff x <= y ) by Lemma01; :: thesis: verum

end;

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

proof

let x, y, z be Element of [.0,1.]; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))
U3: 1 in [.0,1.] by XXREAL_1:1;
U2: ( x <= 1 & y <= 1 ) 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 U1: ( y <= z & x <= z ) ; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))

then O1: I_LK . (x,(I_LK . (y,z))) = I_LK . (x,1) by A1
.= 1 by U2, U3, A1 ;
I_LK . (y,(I_LK . (x,z))) = I_LK . (y,1) by A1, U1
.= 1 by U2, A1, U3 ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by O1; :: thesis: verum

end;

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

then PO: ( I_LK . (x,z) = (1 - x) + z & I_LK . (y,z) = (1 - y) + z ) by Lemma01;

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

suppose P1: x > (1 - y) + z ; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))

then x + y > ((1 + z) - y) + y by XREAL_1:6;
then o9: (x + y) - x > (1 + z) - x by XREAL_1:9;
O1: I_LK . (x,(I_LK . (y,z))) = (1 - x) + ((1 - y) + z) by Lemma01, P1, PO;
I_LK . (y,(I_LK . (x,z))) = (1 - y) + ((1 - x) + z) by Lemma01, o9, PO;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by O1; :: thesis: verum

end;

suppose S1: x <= (1 - y) + z ; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))

then x + y <= ((1 - y) + z) + y by XREAL_1:6;
then O9: (x + y) - x <= (1 + z) - x by XREAL_1:9;
I_LK . (x,(I_LK . (y,z))) = 1 by Lemma01, PO, S1;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by PO, O9, Lemma01; :: thesis: verum

end;

end;

end;

suppose VV: ( y <= z & x > z ) ; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))

then O3: I_LK . (x,z) = (1 - x) + z by Lemma01;
1 - x in [.0,1.] by FUZNORM1:7;
then 1 - x >= 0 by XXREAL_1:1;
then o2: (1 - x) + z >= 0 + z by XREAL_1:6;
I_LK . (x,(I_LK . (y,z))) = I_LK . (x,1) by VV, Lemma01
.= 1 by Lemma01, U2, U3 ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by o2, Lemma01, O3, VV, XXREAL_0:2; :: thesis: verum

end;

suppose VV: ( y > z & x <= z ) ; :: thesis: I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))

then O8: I_LK . (y,z) = (1 - y) + z by Lemma01;
1 - y in [.0,1.] by FUZNORM1:7;
then 0 <= 1 - y by XXREAL_1:1;
then o2: 0 + z <= (1 - y) + z by XREAL_1:6;
I_LK . (y,(I_LK . (x,z))) = I_LK . (y,1) by VV, Lemma01
.= 1 by Lemma01, U2, U3 ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by o2, Lemma01, O8, VV, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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