:: deftheorem defines .--> FUNCOP_1:def 9 :
for x, y being object holds x .--> y = {x} --> y;