let L be upper-bounded Semilattice; :: thesis: for V being Subset of L holds not { x where x is Element of L : V "/\" {x} c= V } is empty
let V be Subset of L; :: thesis: not { x where x is Element of L : V "/\" {x} c= V } is empty
set G = { x where x is Element of L : V "/\" {x} c= V } ;
V "/\" {(Top L)} = V by Th14;
then Top L in { x where x is Element of L : V "/\" {x} c= V } ;
hence not { x where x is Element of L : V "/\" {x} c= V } is empty ; :: thesis: verum