let X be set ; :: thesis: for S being Subset-Family of X
for S1, S2 being set st S1 in S & S2 in S & S is semi-diff-closed holds
ex x being finite Subset of S st x is a_partition of S1 \ S2
let S be Subset-Family of X; :: thesis: for S1, S2 being set st S1 in S & S2 in S & S is semi-diff-closed holds
ex x being finite Subset of S st x is a_partition of S1 \ S2
let S1, S2 be set ; :: thesis: ( S1 in S & S2 in S & S is semi-diff-closed implies ex x being finite Subset of S st x is a_partition of S1 \ S2 )
assume ( S1 in S & S2 in S & S is semi-diff-closed ) ; :: thesis: ex x being finite Subset of S st x is a_partition of S1 \ S2
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: x is a_partition of S1 \ S2

now :: thesis: for p being object st p in x holds
p in bool (S1 \ S2)

let p be object ; :: thesis: ( p in x implies p in bool (S1 \ S2) )
assume U1: p in x ; :: thesis: p in bool (S1 \ S2)
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: verum

end;

then Y5: x c= bool (S1 \ S2) ;
Y3: union x = S1 \ S2 by Y2, PARTIT1:2;

now :: thesis: 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 ) ) )

let A be Subset of (S1 \ S2); :: thesis: ( A in x implies ( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in x or A = B or A misses B ) ) ) )
assume A in x ; :: thesis: ( A <> {} & ( for B being Subset of (S1 \ S2) holds
( not B in x or A = B or A misses B ) ) )
then Y6: ( A in rng F & not A in {{}} ) by XBOOLE_0:def 5;
hence A <> {} by TARSKI:def 1; :: thesis: for B being Subset of (S1 \ S2) holds
( not B in x or A = B or A misses B )

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

let B be Subset of (S1 \ S2); :: thesis: ( not B in x or A = B or A misses B )
assume B in x ; :: thesis: ( A = B or A misses B )
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: verum

end;

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

end;

hence x is a_partition of S1 \ S2 by Y3, Y5, EQREL_1:def 4; :: thesis: verum