let L be Lattice; :: thesis: ( L is 1_Lattice implies {(Top L)} is Filter of L )
assume L is 1_Lattice ; :: thesis: {(Top L)} is Filter of L
then reconsider K = L as 1_Lattice ;
{(Top K)} is Filter of K

proof

let p, q be Element of K; :: according to FILTER_0:def 1 :: thesis: ( ( p in {(Top K)} & q in {(Top K)} ) iff p "/\" q in {(Top K)} )
A1: ( (Top K) "/\" (Top K) = Top K & p "/\" (Top K) = p & (Top K) "/\" q = q & ( p in {(Top K)} implies p = Top K ) & ( p = Top K implies p in {(Top K)} ) & ( q in {(Top K)} implies q = Top K ) & ( q = Top K implies q in {(Top K)} ) & ( p "/\" q in {(Top K)} implies p "/\" q = Top K ) & ( p "/\" q = Top K implies p "/\" q in {(Top K)} ) ) by LATTICES:43, TARSKI:def 1;
hence ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) ; :: thesis: ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) )
assume p "/\" q in {(Top K)} ; :: thesis: ( p in {(Top K)} & q in {(Top K)} )
then ( p "/\" q = Top K & p "/\" q = q "/\" p & p "/\" q [= p & q "/\" p [= q & p [= Top K & q [= Top K ) by LATTICES:23, LATTICES:45, TARSKI:def 1;
hence ( p in {(Top K)} & q in {(Top K)} ) by A1, LATTICES:26; :: thesis: verum

end;

hence {(Top L)} is Filter of L ; :: thesis: verum