for T being non empty TopSpace
for cF3, cF4 being Filter of the carrier of T st cF4 is_filter-finer_than cF3 holds
lim_filter cF3 c= lim_filter cF4