for P being non empty upper-bounded Poset st the InternalRel of P is well-ordering holds
for x, y being Element of P st y < x holds
ex z being Element of P st
( z is compact & y <= z & z <= x )