theorem Lm1: :: SRINGS_3:8

for X being set
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