theorem Th153: :: MEMBER_1:153

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 }