let f be ManySortedSet of X; :: thesis: ( f is d.union-distributive implies f is U-continuous )
dom f = X by PBOOLE:def 3;
hence ( f is d.union-distributive implies f is U-continuous ) by Def14; :: thesis: verum