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

proof

let A, B be set ; :: according to SRINGS_3:def 1 :: thesis:
assume ( A in bool X & B in bool X ) ; :: thesis:
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:

let i, j be object ; :: thesis:
assume A1: i <> j ; :: thesis:

A2: now :: thesis:

assume ( i in dom F & j in dom F ) ; :: thesis:
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:

end;

per cases by A2;

suppose not i in dom F ; :: thesis:

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

end;

suppose not j in dom F ; :: thesis:

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

end;

end;

end;

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

end;