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

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