:: deftheorem defines (B1) ARMSTRNG:def 4 :
for X being set
for B being Subset-Family of X holds
( B is (B1) iff X in B );