let F, G, H be ext-real-membered set ; :: thesis: (F /// G) /// H = F /// (G ** H)
thus (F /// G) /// H = F ** ((G "") ** (H "")) by Th80
.= F /// (G ** H) by Th85 ; :: thesis: verum