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