theorem Th158: :: MEMBER_1:158

for F, G being ext-real-membered set
for r being Real holds r -- (F \ G) = (r -- F) \ (r -- G)