:: deftheorem Def4 defines Irr WAYBEL16:def 4 :
for L being non empty RelStr
for b₂ being Subset of L holds
( b₂ = Irr L iff for x being Element of L holds
( x in b₂ iff x is completely-irreducible ) );