let L be up-complete Semilattice; :: thesis: for D being non empty directed Subset of L

for x being Element of L holds ex_sup_of {x} "/\" D,L

let D be non empty directed Subset of L; :: thesis: for x being Element of L holds ex_sup_of {x} "/\" D,L

let x be Element of L; :: thesis: ex_sup_of {x} "/\" D,L

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

ex_sup_of xx "/\" D,L by WAYBEL_0:75;

hence ex_sup_of {x} "/\" D,L ; :: thesis: verum

for x being Element of L holds ex_sup_of {x} "/\" D,L

let D be non empty directed Subset of L; :: thesis: for x being Element of L holds ex_sup_of {x} "/\" D,L

let x be Element of L; :: thesis: ex_sup_of {x} "/\" D,L

reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;

ex_sup_of xx "/\" D,L by WAYBEL_0:75;

hence ex_sup_of {x} "/\" D,L ; :: thesis: verum