theorem :: MEMBER_1:172

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