let L be up-complete sup-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