let S be Subset-Family of X; :: thesis: ( S is diff-closed implies S is diff-finite-partition-closed )
assume A1: S is diff-closed ; :: thesis: S is diff-finite-partition-closed
for S1, S2 being Element of S st not S1 \ S2 is empty holds
ex y being finite Subset of S st y is a_partition of S1 \ S2
proof
let S1, S2 be Element of S; :: thesis: ( not S1 \ S2 is empty implies ex y being finite Subset of S st y is a_partition of S1 \ S2 )
per cases ( not S is empty or S is empty ) ;
suppose A2: not S is empty ; :: thesis: ( not S1 \ S2 is empty implies ex y being finite Subset of S st y is a_partition of S1 \ S2 )
assume A3: not S1 \ S2 is empty ; :: thesis: ex y being finite Subset of S st y is a_partition of S1 \ S2
take {(S1 \ S2)} ; :: thesis: ( {(S1 \ S2)} is finite Subset of S & {(S1 \ S2)} is a_partition of S1 \ S2 )
{(S1 \ S2)} c= S
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(S1 \ S2)} or x in S )
S1 \ S2 in S by A1, A2;
hence ( not x in {(S1 \ S2)} or x in S ) by TARSKI:def 1; :: thesis: verum
end;
hence ( {(S1 \ S2)} is finite Subset of S & {(S1 \ S2)} is a_partition of S1 \ S2 ) by A3, EQREL_1:39; :: thesis: verum
end;
suppose S is empty ; :: thesis: ( not S1 \ S2 is empty implies ex y being finite Subset of S st y is a_partition of S1 \ S2 )
hence ( not S1 \ S2 is empty implies ex y being finite Subset of S st y is a_partition of S1 \ S2 ) by SUBSET_1:def 1; :: thesis: verum
end;
end;
end;
hence S is diff-finite-partition-closed ; :: thesis: verum