theorem :: CARDFIL2:14

for X being set
for S being Subset-Family of X holds <.S.] = { x where x is Subset of X : ex b being Element of S st b c= x }