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