theorem Th157: :: MEMBER_1:157

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