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