let X be set ; :: thesis:
let S be Subset-Family of X; :: thesis:
assume that
A0: S is with_empty_element and
A1: S is cap-finite-partition-closed and
A2: S is diff-c=-finite-partition-closed ; :: thesis:

now :: thesis:

let S1, S2 be set ; :: thesis:
assume A3: ( S1 in S & S2 in S ) ; :: thesis:

per cases ;

suppose X1: S1 \ S2 <> {} ; :: thesis:

then consider x being finite Subset of S such that
L4: x is a_partition of S1 \ S2 by A1, A2, A3, SRINGS_1:def 2;
L8: ( union x = S1 \ S2 & ( for A being Subset of (S1 \ S2) st A in x holds
( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in x or A = B or A misses B ) ) ) ) ) by L4, EQREL_1:def 4;
L5: rng (canFS x) c= x ;
rng (canFS x) c= S by XBOOLE_1:1;
then reconsider F = canFS x as FinSequence of S by FINSEQ_1:def 4;

now :: thesis:

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

per cases ;

suppose L10: ( i in dom F & j in dom F ) ; :: thesis:

then ( F . i in x & F . j in x ) by L5, FUNCT_1:3;
then ( F . i = F . j or F . i misses F . j ) by L4, EQREL_1:def 4;
hence F . i misses F . j by L6, L10, FUNCT_1:def 4; :: thesis:

end;

suppose ( not i in dom F or not j in dom F ) ; :: thesis:

then ( F . i = {} or 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 S by PROB_2:def 2;
take F = F; :: thesis:
thus Union F = S1 \ S2 by L4, X1, L8, CANFS; :: thesis:

end;

suppose T0: S1 \ S2 = {} ; :: thesis:

set F = canFS {{}};
{{}} c= S by A0, SETFAM_1:def 8, ZFMISC_1:31;
then rng (canFS {{}}) c= S ;
then reconsider F = canFS {{}} as FinSequence of S by FINSEQ_1:def 4;
T3: F = <*{}*> by FINSEQ_1:94;

now :: thesis:

let i, j be object ; :: thesis:
assume i <> j ; :: thesis:
( i in dom F implies i = 1 ) by T3, FINSEQ_1:90;
then F . i = {} by T3, FINSEQ_1:40, FUNCT_1:def 2;
hence F . i misses F . j ; :: thesis:

end;

then reconsider F = F as disjoint_valued FinSequence of S by PROB_2:def 2;
take F = F; :: thesis:
Union F = union {{}} by CANFS;
hence S1 \ S2 = Union F by T0; :: thesis:

end;

end;

end;

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