for L being non empty reflexive transitive RelStr
for x, y being Element of L st x <= y holds
compactbelow x c= compactbelow y