let L be Semilattice; :: thesis: 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
let F be Filter of L; :: thesis: 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
let G be GeneratorSet of F; :: thesis: 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
let A be non empty Subset of L; :: thesis: ( G is_coarser_than A & A is_coarser_than F implies A is GeneratorSet of F )
assume A1: G is_coarser_than A ; :: thesis: ( not A is_coarser_than F or A is GeneratorSet of F )
assume A2: A is_coarser_than F ; :: thesis: A is GeneratorSet of F
F = uparrow (fininfs G) by Def3;
hence F c= uparrow (fininfs A) by A1, Th4, Th29; :: according to XBOOLE_0:def 10,WAYBEL12:def 3 :: thesis: uparrow (fininfs A) c= F
A c= F by A2, YELLOW_4:8;
hence uparrow (fininfs A) c= F by WAYBEL_0:62; :: thesis: verum