let X be non empty set ; :: thesis: for F being Filter of X
for B being non empty Subset of F holds
( F is_coarser_than B iff B is filter_basis )
let F be Filter of X; :: thesis: for B being non empty Subset of F holds
( F is_coarser_than B iff B is filter_basis )
let B be non empty Subset of F; :: thesis: ( F is_coarser_than B iff B is filter_basis )
hereby :: thesis: ( B is filter_basis implies F is_coarser_than B )
assume A1: F is_coarser_than B ; :: thesis: B is filter_basis
now :: thesis: for f being Element of F ex b being Element of B st b c= f
let f be Element of F; :: thesis: ex b being Element of B st b c= f
consider b being set such that
A2: b in B and
A3: b c= f by A1;
reconsider b1 = b as Element of B by A2;
( b1 is Element of B & b1 c= f ) by A3;
hence ex b being Element of B st b c= f ; :: thesis: verum
end;
hence B is filter_basis ; :: thesis: verum
end;
assume A4: B is filter_basis ; :: thesis: F is_coarser_than B
for f being set st f in F holds
ex b being set st
( b in B & b c= f )
proof
let f be set ; :: thesis: ( f in F implies ex b being set st
( b in B & b c= f ) )
assume f in F ; :: thesis: ex b being set st
( b in B & b c= f )
then consider b being Element of B such that
A5: b c= f by A4;
thus ex b being set st
( b in B & b c= f ) by A5; :: thesis: verum
end;
hence F is_coarser_than B ; :: thesis: verum