theorem Th137: :: MEMBER_1:137

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