:: deftheorem Def13 defines U-continuous COHSP_1:def 13 :
for f being Function holds
( f is U-continuous iff ( dom f is d.union-closed & f is d.union-distributive ) );