let L be Lattice; :: thesis: for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
let F be Filter of L; :: thesis: ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) )
F = <.F.) by Th21;
hence ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) by Th25; :: thesis: verum