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