theorem Th21: :: WAYBEL_3:21

for L being non empty up-complete Poset
for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds
x in I ) holds
x << y