for T being non empty 1-sorted holds
( T is real-membered iff for x being Element of T holds x is real )