let L be upper-bounded Semilattice; :: thesis: for F being non empty directed Subset of (InclPoset (Filt L)) holds sup F = union F
let F be non empty directed Subset of (InclPoset (Filt L)); :: thesis: sup F = union F
Filt L = Ids (L opp) by WAYBEL16:7;
hence sup F = union F by WAYBEL13:9; :: thesis: verum