let L be Semilattice; :: thesis: for S being non empty upper Subset of L holds
( S is Filter of L iff S is meet-closed )
let S be non empty upper Subset of L; :: thesis: ( S is Filter of L iff S is meet-closed )
( S is Filter of L iff subrelstr S is meet-inheriting ) by WAYBEL_0:63;
hence ( S is Filter of L iff S is meet-closed ) by Def1; :: thesis: verum