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
set i = the Element of I;
the Element of I is Element of L ;
hence ex p being Element of L st p in I ; :: thesis: verum