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 ;

now

let p, q be Element of K; :: thesis: ( ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) & ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) ) )
A1: ( p [= Top K & q [= Top K ) by LATTICES:19;
A2: ( p in {(Top K)} iff p = Top K ) by TARSKI:def 1;
hence ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) by LATTICES:17; :: 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 A3: p "/\" q = Top K by TARSKI:def 1;
( p "/\" q [= p & q "/\" p [= q ) by LATTICES:6;
hence ( p in {(Top K)} & q in {(Top K)} ) by A2, A3, A1, LATTICES:8; :: thesis: verum

end;

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