:: deftheorem defines --> FUNCOP_1:def 2 :
for A being set
for z being object holds A --> z = [:A,{z}:];