let X, I be non empty set ; :: thesis: for M being Filt X -valued ManySortedSet of I
for i being Element of I
for F being Filter of X st F = M . i holds
Filter_Intersection M is_filter-coarser_than F
let M be Filt X -valued ManySortedSet of I; :: thesis: for i being Element of I
for F being Filter of X st F = M . i holds
Filter_Intersection M is_filter-coarser_than F
let i be Element of I; :: thesis: for F being Filter of X st F = M . i holds
Filter_Intersection M is_filter-coarser_than F
let F be Filter of X; :: thesis: ( F = M . i implies Filter_Intersection M is_filter-coarser_than F )
set FIM = Filter_Intersection M;
assume A1: F = M . i ; :: thesis: Filter_Intersection M is_filter-coarser_than F

now :: thesis: for a being object st a in Filter_Intersection M holds
a in F

let a be object ; :: thesis: ( a in Filter_Intersection M implies a in F )
assume A2: a in Filter_Intersection M ; :: thesis: a in F
i in I ;
then i in dom M by PARTFUN1:def 2;
then M . i in rng M by FUNCT_1:def 3;
hence a in F by A1, A2, SETFAM_1:def 1; :: thesis: verum

end;

then Filter_Intersection M c= F ;
hence Filter_Intersection M is_filter-coarser_than F ; :: thesis: verum