theorem Th83: :: MEMBER_1:83

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