theorem :: ARMSTRNG:45

for X, G being set
for B being non empty finite Subset-Family of X st B is (B1) & B is (B2) & G is_generator-set_of B holds
/\-IRR B c= G \/ {X}