let X be set ; :: thesis: for S being non empty Subset-Family of X st S is semi-diff-closed holds
S is diff-c=-finite-partition-closed
let S be non empty Subset-Family of X; :: thesis: ( S is semi-diff-closed implies S is diff-c=-finite-partition-closed )
assume S is semi-diff-closed ; :: thesis: S is diff-c=-finite-partition-closed
then for S1, S2 being Element of S st S2 c= S1 holds
ex x being finite Subset of S st x is a_partition of S1 \ S2 by Lm1;
hence S is diff-c=-finite-partition-closed by SRINGS_1:def 3; :: thesis: verum