for L being non empty upper-bounded Poset
for R being auxiliary(ii) Relation of L
for C being strict_chain of R
for m being Element of L st C is maximal & m is_maximum_of C & [m,(Top L)] in R holds
( [(Top L),(Top L)] in R & m = Top L )