theorem Th20: :: MEMBERED:20

for X being set
for Y being ext-real-membered set st X c= Y holds
X is ext-real-membered ;