for O being non empty connected Poset
for x, y being Element of O holds
( x > y iff not x <= y )