let L be Lattice; :: thesis: for H being Filter of L st L is 1_Lattice holds
Top L in H
let H be Filter of L; :: thesis: ( L is 1_Lattice implies Top L in H )
assume L is 1_Lattice ; :: thesis: Top L in H
then reconsider L = L as 1_Lattice ;
consider p being Element of L such that
A1: p in H by SUBSET_1:4;
p [= Top L by LATTICES:19;
hence Top L in H by A1, Th9; :: thesis: verum