theorem Th5: :: WAYBEL_8:5

for L being non empty reflexive RelStr
for x being Element of L holds compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L)