theorem Th42: :: MEMBER_1:42

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