:: deftheorem defines [#] STRUCT_0:def 3 :
for T being 1-sorted holds [#] T = the carrier of T;