for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for F being FinSequence of S
for G being Element of S ex H being disjoint_valued FinSequence of S st G \ (Union F) = Union H