for L being non empty reflexive antisymmetric RelStr
for x, y being Element of L st x <= y holds
( sup {x,y} = y & inf {x,y} = x )