for x, y being Element of [.0,1.] holds
( ( x <= y implies I_LK . (x,y) = 1 ) & ( x > y implies I_LK . (x,y) = (1 - x) + y ) )