theorem Th16: :: LATTICEA:11

for L being Lattice
for a being Element of L holds { F where F is Filter of L : ( F is prime & a in F ) } c= PFilters L