theorem Th21: :: MEMBER_1:21

for F being ext-real-membered set
for f being ExtReal st f in F holds
f " in F ""