:: deftheorem Def8 defines real-membered TOPMETR:def 8 :
for T being 1-sorted holds
( T is real-membered iff the carrier of T is real-membered );