theorem Th39: :: ARMSTRNG:39

for X being set
for K being Subset of X
for B being Subset-Family of X st B = {X} \/ { A where A is Subset of X : not K c= A } holds
( B is (B1) & B is (B2) )