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

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