:: deftheorem Def4 defines Imf FUZZY_4:def 4 :
for C1, C2 being non empty set
for b3 being RMembership_Func of C1,C2 holds
( b3 = Imf (C1,C2) iff for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies b3 . (x,y) = 1 ) & ( x <> y implies b3 . (x,y) = 0 ) ) );