:: deftheorem defines --> STRUCT_0:def 14 :
for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;