let L be Lattice; :: thesis: the carrier of L is Filter of L
the carrier of L c= the carrier of L ;
then reconsider FL = the carrier of L as non empty Subset of L ;
FL is Filter of L

proof

thus for p, q being Element of L holds
( ( p in FL & q in FL ) iff p "/\" q in FL ) ; :: according to FILTER_0:def 1 :: thesis: verum

end;

hence the carrier of L is Filter of L ; :: thesis: verum