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

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