let R be set ; :: thesis: ( R is diff-closed implies ( R is semi-diff-closed & R is cap-closed ) )
assume A1: R is diff-closed ; :: thesis: ( R is semi-diff-closed & R is cap-closed )

now :: thesis: for A, B being set st A in R & B in R holds
ex F being disjoint_valued FinSequence of R st A \ B = Union F

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

now :: thesis: for x, y being object st x <> y holds
F . x misses F . y

let x, y be object ; :: thesis: ( x <> y implies F . b₁ misses F . b₂ )
assume A3: x <> y ; :: thesis: F . b₁ misses F . b₂
A4: dom F = {1} by FINSEQ_1:2, FINSEQ_1:38;

per cases ( x in dom F or not x in dom F ) ;

suppose x in dom F ; :: thesis: F . b₁ misses F . b₂

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: verum

end;

suppose not x in dom F ; :: thesis: F . b₁ misses F . b₂

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

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: verum

end;

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

now :: thesis: for A, B being set st A in R & B in R holds
A /\ B in R

let A, B be set ; :: thesis: ( A in R & B in R implies A /\ B in R )
assume A6: ( A in R & B in R ) ; :: thesis: A /\ B in R
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: verum

end;

hence R is cap-closed ; :: thesis: verum