set I = I_LK ;

A1: I_LK is satisfying_(OP)

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

A1: I_LK is satisfying_(OP)

proof

for x, y, z being Element of [.0,1.] holds I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z)))
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 )

end;( I_LK . (x,y) = 1 implies x <= y )

proof

hence
( I_LK . (x,y) = 1 iff x <= y )
by Lemma01; :: thesis: verum
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;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

proof

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

end;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 ) )
;

end;

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;.= 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

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;

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

end;

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;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

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;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

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;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

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;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

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