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 Th26;
hence ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) by Th31; :: thesis: verum