:: deftheorem Def19 defines -element STRUCT_0:def 19 :
for C being set
for X being 1-sorted holds
( X is C -element iff the carrier of X is C -element );