theorem Th1: :: WAYBEL23:1

for L being non empty Poset
for x being Element of L holds compactbelow x = (waybelow x) /\ the carrier of (CompactSublatt L)