theorem Th13: :: WAYBEL_3:13

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