theorem Th224: :: MEMBER_1:224

for F being ext-real-membered set
for f being ExtReal holds F /// f = { (w / f) where w is Element of ExtREAL : w in F }