theorem Th190: :: MEMBER_1:190

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