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