theorem Th18: :: WAYBEL_3:18

for L being complete LATTICE
for x, y being Element of L st x << y holds
for X being Subset of L st y <= sup X holds
ex A being finite Subset of L st
( A c= X & x <= sup A )