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 ;
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 ;
I_LK . (y,(I_LK . (x,z))) = (1 - y) + ((1 - x) + z) by ;
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 ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by ; :: 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
.= 1 by ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by ; :: 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
.= 1 by ;
hence I_LK . (x,(I_LK . (y,z))) = I_LK . (y,(I_LK . (x,z))) by ; :: 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