:: deftheorem defines {} STRUCT_0:def 2 :
for T being 1-sorted holds {} T = {} ;