:: deftheorem defines in STRUCT_0:def 5 :
for S being 1-sorted
for x being object holds
( x in S iff x in the carrier of S );