let L be Lattice; :: thesis: for F being Filter of L holds F is ClosedSubset of L
let F be Filter of L; :: thesis: F is ClosedSubset of L
for p, q being Element of L st p in F & q in F holds
( p "/\" q in F & p "\/" q in F ) by FILTER_0:10, FILTER_0:def 1;
hence F is ClosedSubset of L by Def10; :: thesis: verum