for L being up-complete Chain
for x, y being Element of L st x < y holds
x << y