theorem :: MEMBER_1:25

for F being ext-real-membered set holds -- (F "") = (-- F) ""