let X be non empty set ; :: thesis: for FB being filter_base of X
for F being Filter of X st FB c= F holds
<.FB.) is_coarser_than F
let FB be filter_base of X; :: thesis: for F being Filter of X st FB c= F holds
<.FB.) is_coarser_than F
let F be Filter of X; :: thesis: ( FB c= F implies <.FB.) is_coarser_than F )
assume A1: FB c= F ; :: thesis: <.FB.) is_coarser_than F

now :: thesis: for x being object st x in <.FB.) holds
x in F

let x be object ; :: thesis: ( x in <.FB.) implies x in F )
assume A2: x in <.FB.) ; :: thesis: x in F
then reconsider x1 = x as Subset of X ;
consider b being Element of FB such that
A4: b c= x1 by A2, def3;
A5: b in F by A1;
reconsider x2 = x1 as Subset of X ;
consider c being Element of F such that
A6: c c= x2 by A4, A5;
thus x in F by A6, CARD_FIL:def 1; :: thesis: verum

end;

hence <.FB.) is_coarser_than F ; :: thesis: verum