:: deftheorem defines completely-irreducible WAYBEL16:def 3 :
for L being non empty RelStr
for p being Element of L holds
( p is completely-irreducible iff ex_min_of (uparrow p) \ {p},L );