let X be non empty set ; :: thesis: for F1, F2 being Filter of X
for B1 being basis of F1
for B2 being basis of F2 holds
( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )
let F1, F2 be Filter of X; :: thesis: for B1 being basis of F1
for B2 being basis of F2 holds
( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )
let B1 be basis of F1; :: thesis: for B2 being basis of F2 holds
( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )
let B2 be basis of F2; :: thesis: ( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )

hereby :: thesis: ( B1 is_coarser_than B2 implies F1 is_filter-coarser_than F2 )

assume F1 is_filter-coarser_than F2 ; :: thesis: B1 is_coarser_than B2
then A1: F1 c= F2 ;

now :: thesis: for x being set st x in B1 holds
ex y being set st
( y in B2 & y c= x )

let x be set ; :: thesis: ( x in B1 implies ex y being set st
( y in B2 & y c= x ) )
assume x in B1 ; :: thesis: ex y being set st
( y in B2 & y c= x )
then x in F2 by A1;
then ex b being Element of B2 st b c= x by def2;
hence ex y being set st
( y in B2 & y c= x ) ; :: thesis: verum

end;

hence B1 is_coarser_than B2 ; :: thesis: verum

end;

assume A2: B1 is_coarser_than B2 ; :: thesis: F1 is_filter-coarser_than F2

now :: thesis: for x being object st x in F1 holds
x in F2

let x be object ; :: thesis: ( x in F1 implies x in F2 )
assume A3: x in F1 ; :: thesis: x in F2
then reconsider x1 = x as Subset of X ;
consider b1 being Element of B1 such that
A4: b1 c= x1 by A3, def2;
consider b2 being set such that
A5: b2 in B2 and
A6: b2 c= b1 by A2;
reconsider b2 = b2 as Element of B2 by A5;
A7: b2 c= x1 by A4, A6;
x1 in <.(# B2).] by A7, def3;
hence x in F2 by Th06; :: thesis: verum

end;

then F1 c= F2 ;
hence F1 is_filter-coarser_than F2 ; :: thesis: verum