for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x is Subset of (CompactSublatt L)