let L be Lattice; :: thesis: for I being Ideal of L ex p being Element of L st p in I
let I be Ideal of L; :: thesis: ex p being Element of L st p in I
consider i being Element of I;
i is Element of L ;
hence ex p being Element of L st p in I ; :: thesis: verum