:: deftheorem Def12 defines cap-distributive COHSP_1:def 12 :
for f being Function holds
( f is cap-distributive iff for a, b being set st dom f includes_lattice_of a,b holds
f . (a /\ b) = (f . a) /\ (f . b) );