theorem HelpMaxPrime: :: LATTICEA:15

for L being Lattice
for F being Filter of L
for a being Element of L
for G being set st G = { x where x is Element of L : ex u being Element of L st
( u in F & a "/\" u [= x ) } & a in G holds
G is Filter of L