:: deftheorem defines id STRUCT_0:def 4 :
for S being 1-sorted holds id S = id the carrier of S;