let x, y be Element of [.0,1.]; ( ( x <= y implies I_LK . (x,y) = 1 ) & ( x > y implies I_LK . (x,y) = (1 - x) + y ) )
thus
( x <= y implies I_LK . (x,y) = 1 )
( x > y implies I_LK . (x,y) = (1 - x) + y )
assume
x > y
; I_LK . (x,y) = (1 - x) + y
then
1 - x <= 1 - y
by XREAL_1:10;
then a1:
(1 - x) + y <= (1 - y) + y
by XREAL_1:6;
I_LK . (x,y) =
min (1,((1 - x) + y))
by FUZIMPL1:def 14
.=
(1 - x) + y
by a1, XXREAL_0:def 9
;
hence
I_LK . (x,y) = (1 - x) + y
; verum