theorem Th1: :: WAYBEL14:1

for X being set
for F being finite Subset-Family of X ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )