let X be set ; :: thesis: for S being Subset-Family of X st S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed holds
S is semi-diff-closed
let S be Subset-Family of X; :: thesis: ( S is with_empty_element & S is cap-finite-partition-closed & S is diff-c=-finite-partition-closed implies S is semi-diff-closed )
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: S is semi-diff-closed

now :: thesis: for S1, S2 being set st S1 in S & S2 in S holds
ex F being disjoint_valued FinSequence of S st Union F = S1 \ S2

let S1, S2 be set ; :: thesis: ( S1 in S & S2 in S implies ex F being disjoint_valued FinSequence of S st Union b₃ = F \ b₂ )
assume A3: ( S1 in S & S2 in S ) ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b₃ = F \ b₂

per cases ( S1 \ S2 <> {} or S1 \ S2 = {} ) ;

suppose X1: S1 \ S2 <> {} ; :: thesis: ex F being disjoint_valued FinSequence of S st Union b₃ = F \ b₂

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: 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 L6: i <> j ; :: thesis: F . b₁ misses F . b₂

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

suppose L10: ( i in dom F & j in dom F ) ; :: thesis: F . b₁ misses F . b₂

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

end;

suppose ( not i in dom F or not j in dom F ) ; :: thesis: F . b₁ misses F . b₂

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

end;

suppose T0: S1 \ S2 = {} ; :: thesis: ex F being disjoint_valued FinSequence of S st F \ b₂ = Union b₃

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: for i, j being object st i <> j holds
F . i misses F . j

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

end;

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

end;

end;

end;

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