theorem HelpMaxPrime2: :: LATTICEA:16

for L being Lattice
for F being Ideal 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 & x [= a "\/" u ) } & a in G holds
G is Ideal of L