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

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