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 :: thesis: for p, q being Element of K holds
( ( 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)} ) ) )

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 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)} ) ; :: 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 A2: 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 A1, A2; :: thesis: verum

end;

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