theorem Th139: :: MEMBER_1:139

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