theorem Th80: :: MEMBER_1:80

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