let L be Lattice; :: thesis: for F being Filter of L holds <.F.) = F
let F be Filter of L; :: thesis: <.F.) = F
for H being Filter of L st F c= H holds
F c= H ;
hence <.F.) = F by Def5; :: thesis: verum