for L being non empty reflexive RelStr
for x, y being Element of L holds
( y in compactbelow x iff ( x >= y & y is compact ) )