theorem Th211: :: MEMBER_1:211

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