for X being real-membered set st ( for r being Real holds r in X ) holds
X = REAL