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 set 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 BORSUK_4:def 2; :: thesis: verum