theorem Th138: :: MEMBER_1:138

for F, G being ext-real-membered set
for f being ExtReal holds (f ++ F) \ (f ++ G) c= f ++ (F \ G)