let x, y be Element of [.0,1.]; :: thesis: ( ( 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 ) :: thesis: ( x > y implies I_LK . (x,y) = (1 - x) + y )
proof
assume x <= y ; :: thesis: I_LK . (x,y) = 1
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 by a1, XXREAL_0:def 9 ;
hence I_LK . (x,y) = 1 ; :: thesis: verum
end;
assume x > y ; :: thesis: 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 ; :: thesis: verum