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