theorem Th11: :: TAXONOM2:12

for Y being set
for S1 being Subset of Y
for B being mutually-disjoint Subset-Family of Y st ( for b being set st b in B holds
( S1 misses b & Y <> {} ) ) holds
( B \/ {S1} is mutually-disjoint Subset-Family of Y & ( S1 <> {} implies union (B \/ {S1}) <> union B ) )