for L being complete LATTICE
for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y