let L be up-complete sup-Semilattice; :: thesis: for D being non empty directed Subset of
for x being Element of holds ex_sup_of {x} "\/" D,L
let D be non empty directed Subset of ; :: thesis: for x being Element of holds ex_sup_of {x} "\/" D,L
let x be Element of ; :: thesis: ex_sup_of {x} "\/" D,L
reconsider xx = {x} as non empty directed Subset of by WAYBEL_0:5;
ex_sup_of xx "\/" D,L by WAYBEL_0:75;
hence ex_sup_of {x} "\/" D,L ; :: thesis: verum