:: deftheorem Def3 defines /\-IRR ARMSTRNG:def 3 :
for X being non empty set
for b₂ being Subset of X holds
( b₂ = /\-IRR X iff for x being set holds
( x in b₂ iff x is_/\-irreducible_in X ) );