:: deftheorem defines In STRUCT_0:def 22 :
for x being object
for S being 1-sorted holds In (x,S) = In (x, the carrier of S);