let R be set ; :: thesis:
assume A1: R is diff-closed ; :: thesis:

now :: thesis:

let A, B be set ; :: thesis:
assume ( A in R & B in R ) ; :: thesis:
then A \ B in R by A1;
then reconsider F = <*(A \ B)*> as FinSequence of R by FINSEQ_1:74;

now :: thesis:

let x, y be object ; :: thesis:
assume A3: x <> y ; :: thesis:
A4: dom F = {1} by FINSEQ_1:2, FINSEQ_1:38;

per cases ;

suppose x in dom F ; :: thesis:

then x = 1 by A4, TARSKI:def 1;
then not y in dom F by A3, A4, TARSKI:def 1;
then F . y = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis:

end;

suppose not x in dom F ; :: thesis:

then F . x = {} by FUNCT_1:def 2;
hence F . x misses F . y ; :: thesis:

end;

end;

end;

then A5: F is disjoint_valued by PROB_2:def 2;
rng F = {(A \ B)} by FINSEQ_1:38;
then Union F = A \ B ;
hence ex F being disjoint_valued FinSequence of R st A \ B = Union F by A5; :: thesis:

end;

hence R is semi-diff-closed ; :: thesis:

now :: thesis:

let A, B be set ; :: thesis:
assume A6: ( A in R & B in R ) ; :: thesis:
then A \ B in R by A1;
then A \ (A \ B) in R by A1, A6;
hence A /\ B in R by XBOOLE_1:48; :: thesis:

end;

hence R is cap-closed ; :: thesis: