theorem :: FILTER_0:12

for L being Lattice st L is 1_Lattice holds
{(Top L)} is Filter of L