let X be set ; :: thesis: bool X is semi-diff-closed
set S = bool X;
thus bool X is semi-diff-closed :: thesis: verum

proof

let A, B be set ; :: according to SRINGS_3:def 1 :: thesis: ( A in bool X & B in bool X implies ex F being disjoint_valued FinSequence of bool X st A \ B = Union F )
assume ( A in bool X & B in bool X ) ; :: thesis: ex F being disjoint_valued FinSequence of bool X st A \ B = Union F
then A \ B c= X by XBOOLE_1:1;
then {(A \ B)} c= bool X by ZFMISC_1:31;
then rng <*(A \ B)*> c= bool X by FINSEQ_1:38;
then reconsider F = <*(A \ B)*> as FinSequence of bool X by FINSEQ_1:def 4;

now :: thesis: for i, j being object st i <> j holds
F . i misses F . j

let i, j be object ; :: thesis: ( i <> j implies F . b₁ misses F . b₂ )
assume A1: i <> j ; :: thesis: F . b₁ misses F . b₂

A2: now :: thesis: ( i in dom F implies not j in dom F )

assume ( i in dom F & j in dom F ) ; :: thesis: contradiction
then ( i in {1} & j in {1} ) by FINSEQ_1:2, FINSEQ_1:38;
then ( i = 1 & j = 1 ) by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum

end;

per cases ( not i in dom F or not j in dom F ) by A2;

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

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

end;

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

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

end;

end;

end;

then reconsider F = F as disjoint_valued FinSequence of bool X by PROB_2:def 2;
take F ; :: thesis: A \ B = Union F
union (rng F) = union {(A \ B)} by FINSEQ_1:38;
hence A \ B = Union F ; :: thesis: verum

end;