theorem Th3: :: MEMBERED:3

for X being set st X is real-membered holds
X c= REAL