let L be Lattice; :: thesis: the carrier of L is Filter of L
the carrier of L = [#] L ;
hence the carrier of L is Filter of L ; :: thesis: verum