theorem :: MEMBER_1:171

for F being ext-real-membered set
for f being ExtReal holds F -- f = -- (f -- F) by Th60;