:: deftheorem defines is_/\-irreducible_in ARMSTRNG:def 2 :
for x, X being set holds
( x is_/\-irreducible_in X iff ( x in X & ( for z, y being set st z in X & y in X & x = z /\ y & not x = z holds
x = y ) ) );