theorem Th7: :: MEMBER_1:7
for F, G being ext-real-membered set holds -- (F \ G) = (-- F) \ (-- G)