let f be Function; :: thesis:
assume A1: ( dom f is subset-closed & dom f is d.union-closed ) ; :: thesis:

hereby :: thesis:

assume f is U-stable ; :: thesis:
then reconsider f' = f as U-stable Function ;
A2: ( dom f' is multiplicative & f' is U-continuous & f' is cap-distributive ) ;
set C = dom f';
thus f is c=-monotone by A2; :: thesis:
let a, y be set ; :: thesis:
assume A3: ( a in dom f & y in f . a ) ; :: thesis:
then consider b being set such that
A4: ( b is finite & b c= a & y in f' . b ) by A1, Th22;
b c= b ;
then b in { c where c is Subset of b : y in f . c } by A4;
then reconsider A = { c where c is Subset of b : y in f . c } as non empty set ;
( bool b is finite & A c= bool b )

thus bool b is finite by A4; :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in A ; :: thesis:
then ex c being Subset of b st
( x = c & y in f . c ) ;
hence x in bool b ; :: thesis:

end;

then reconsider A = A as non empty finite set ;
defpred S₁[ set , set ] means $1 c= $2;
A5: A <> {} ;
A6: for x, y being set st S₁[x,y] & S₁[y,x] holds
x = y by XBOOLE_0:def 10;
A7: for x, y, z being set st S₁[x,y] & S₁[y,z] holds
S₁[x,z] by XBOOLE_1:1;
consider c being set such that
A8: ( c in A & ( for y being set st y in A & y <> c holds
not S₁[y,c] ) ) from CARD_3:sch 2(A5, A6, A7);
take c = c; :: thesis:
ex d being Subset of b st
( c = d & y in f . d ) by A8;
then reconsider c' = c as Subset of b ;
A9: ex d being Subset of b st
( c = d & y in f . d ) by A8;
reconsider c' = c' as finite Subset of b by A4;
thus A10: ( c is finite & c c= a & y in f . c ) by A4, A9, XBOOLE_1:1; :: thesis:
let d be set ; :: thesis:
assume A11: ( d c= a & y in f . d ) ; :: thesis:
then A12: ( c /\ d c= c' & c /\ d c= d & c \/ d c= a & c' in dom f' ) by A1, A3, A10, CLASSES1:def 1, XBOOLE_1:8, XBOOLE_1:17;
then ( d in dom f' & c /\ d in dom f & c \/ d in dom f ) by A1, A3, A11, CLASSES1:def 1;
then dom f includes_lattice_of c,d by A12, Th17;
then ( f . (c /\ d) = (f . c) /\ (f . d) & c /\ d c= b ) by A12, Def13, XBOOLE_1:1;
then ( y in f . (c /\ d) & c /\ d is finite Subset of b ) by A4, A9, A11, XBOOLE_0:def 4;
then c /\ d in A ;
hence c c= d by A8, A12; :: thesis:

end;

assume that
A13: f is c=-monotone and
A14: for a, y being set st a in dom f & y in f . a holds
ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) ; :: thesis:
reconsider C = dom f as subset-closed d.union-closed set by A1;
C is subset-closed set ;
hence dom f is multiplicative ; :: according to COHSP_1:def 15 :: thesis:

let a, y be set ; :: thesis:
assume ( a in dom f & y in f . a ) ; :: thesis:
then ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) ) by A14;
hence ex b being set st
( b is finite & b c= a & y in f . b ) ; :: thesis:

end;

hence f is U-continuous by A1, A13, Th22; :: thesis:
thus f is cap-distributive :: thesis:

let a, b be set ; :: according to COHSP_1:def 13 :: thesis:
assume dom f includes_lattice_of a,b ; :: thesis:
then A15: ( a in dom f & b in dom f & a /\ b in dom f & a \/ b in dom f ) by Th17;
( a /\ b c= a & a /\ b c= b ) by XBOOLE_1:17;
then ( f . (a /\ b) c= f . a & f . (a /\ b) c= f . b ) by A13, A15, Def12;
hence f . (a /\ b) c= (f . a) /\ (f . b) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in (f . a) /\ (f . b) ; :: thesis:
then A16: ( x in f . a & x in f . b ) by XBOOLE_0:def 4;
( a c= a \/ b & b c= a \/ b ) by XBOOLE_1:7;
then f . a c= f . (a \/ b) by A13, A15, Def12;
then consider c being set such that
A17: ( c is finite & c c= a \/ b & x in f . c & ( for d being set st d c= a \/ b & x in f . d holds
c c= d ) ) by A14, A15, A16;
( c c= a & c c= b & C = dom f ) by A16, A17, XBOOLE_1:7;
then ( c c= a /\ b & c in dom f ) by A15, CLASSES1:def 1, XBOOLE_1:19;
then f . c c= f . (a /\ b) by A13, A15, Def12;
hence x in f . (a /\ b) by A17; :: thesis:

end;