let L be sup-Semilattice; :: thesis: for S being join-closed Subset of L holds S is directed

let S be join-closed Subset of L; :: thesis: S is directed

subrelstr S is join-inheriting by Def2;

hence S is directed by YELLOW12:27; :: thesis: verum

let S be join-closed Subset of L; :: thesis: S is directed

subrelstr S is join-inheriting by Def2;

hence S is directed by YELLOW12:27; :: thesis: verum