let X be set ; :: thesis:
let S be Subset-Family of X; :: thesis:
let S1, S2 be set ; :: thesis:
assume ( S1 in S & S2 in S & S is semi-diff-closed ) ; :: thesis:
then consider F being disjoint_valued FinSequence of S such that
Y2: S1 \ S2 = Union F ;
reconsider x = (rng F) \ {{}} as finite Subset of S ;
take x ; :: thesis:

let p be object ; :: thesis:
assume U1: p in x ; :: thesis:
then p in S ;
then reconsider p1 = p as Subset of X ;
( p in rng F & not p in {{}} ) by U1, XBOOLE_0:def 5;
then p1 c= S1 \ S2 by Y2, TARSKI:def 4;
hence p in bool (S1 \ S2) ; :: thesis:

end;

let B be Subset of (S1 \ S2); :: thesis:
assume B in x ; :: thesis:
then ( B in rng F & not B in {{}} ) by XBOOLE_0:def 5;
then ( ex i being Nat st
( i in dom F & F . i = A ) & ex j being Nat st
( j in dom F & F . j = B ) ) by Y6, FINSEQ_2:10;
hence ( A = B or A misses B ) by PROB_2:def 2; :: thesis:

end;

hence for B being Subset of (S1 \ S2) holds
( not B in x or A = B or A misses B ) ; :: thesis:

end;