theorem Th20: :: WAYBEL16:20

for L being non empty Poset
for p being Element of L holds
( p is completely-irreducible iff ex q being Element of L st
( p < q & ( for s being Element of L st p < s holds
q <= s ) & uparrow p = {p} \/ (uparrow q) ) )