let L be Lattice; :: thesis: for H being Filter of L ex p being Element of L st p in H
let H be Filter of L; :: thesis: ex p being Element of L st p in H
consider x being Element of H;
x is Element of L ;
hence ex p being Element of L st p in H ; :: thesis: verum