:: deftheorem Def1 defines complex-functions-membered TOPREALC:def 1 :
for S being 1-sorted holds
( S is complex-functions-membered iff the carrier of S is complex-functions-membered );