let f be ManySortedSet of X; :: thesis: ( f is U-continuous & f is cap-distributive implies f is U-stable )
dom f = X by PARTFUN1:def 2;
hence ( f is U-continuous & f is cap-distributive implies f is U-stable ) by Def15; :: thesis: verum