let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for B1, B2 being filter_base of X st B1 is_coarser_than B2 holds
<.B1.) is_filter-coarser_than <.B2.)
let f be Function of X,Y; :: thesis: for B1, B2 being filter_base of X st B1 is_coarser_than B2 holds
<.B1.) is_filter-coarser_than <.B2.)
let B1, B2 be filter_base of X; :: thesis: ( B1 is_coarser_than B2 implies <.B1.) is_filter-coarser_than <.B2.) )
assume A1: B1 is_coarser_than B2 ; :: thesis: <.B1.) is_filter-coarser_than <.B2.)
( B1 is basis of <.B1.) & B2 is basis of <.B2.) ) by Th10;
hence <.B1.) is_filter-coarser_than <.B2.) by A1, Th11; :: thesis: verum