let T be non empty 1-sorted ; :: thesis: ( T is real-membered iff for x being Element of T holds x is real )
thus ( T is real-membered implies for x being Element of T holds x is real ) ; :: thesis: ( ( for x being Element of T holds x is real ) implies T is real-membered )
assume for x being Element of T holds x is real ; :: thesis: T is real-membered
then for x being object st x in the carrier of T holds
x is real ;
then the carrier of T is real-membered by MEMBERED:def 3;
hence T is real-membered by TOPMETR:def 8; :: thesis: verum