theorem Th30: :: WAYBEL12:30

for L being Semilattice
for F being Filter of L
for G being GeneratorSet of F
for A being non empty Subset of L st G is_coarser_than A & A is_coarser_than F holds
A is GeneratorSet of F