theorem Lem1: :: LATTICEA:13

for L being Lattice
for F being Filter of L st not F is prime holds
ex a, b being Element of L st
( a "\/" b in F & not a in F & not b in F )