theorem Th23: :: WAYBEL12:23

for L being upper-bounded Semilattice
for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty