theorem Th23: :: COHSP_1:23

for f being Function st dom f is subset-closed & dom f is d.union-closed holds
( f is U-linear iff ( f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ) ) )