:: deftheorem def3 defines <. CARDFIL2:def 8 :
for X being set
for B, b₃ being Subset-Family of X holds
( b₃ = <.B.] iff for x being Subset of X holds
( x in b₃ iff ex b being Element of B st b c= x ) );