:: deftheorem defines DisUnion SRINGS_3:def 3 :
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S = { A where A is Subset of X : ex F being disjoint_valued FinSequence of S st A = Union F } ;