theorem Th21: :: FILTER_0:21

for L being Lattice
for F being Filter of L holds <.F.) = F by Def4;