:: deftheorem Def3 defines GeneratorSet WAYBEL12:def 3 :
for L being Semilattice
for F being Filter of L
for b₃ being Subset of L holds
( b₃ is GeneratorSet of F iff F = uparrow (fininfs b₃) );