let L be Semilattice; :: thesis: for S being meet-closed Subset of L holds S is filtered
let S be meet-closed Subset of L; :: thesis: S is filtered
subrelstr S is meet-inheriting by Def1;
hence S is filtered by YELLOW12:26; :: thesis: verum