let L be complete LATTICE; :: thesis: for F being ultra Filter of (BoolePoset ([#] L))
for M being subnet of a_net F holds lim_inf F = lim_inf M
let F be ultra Filter of (BoolePoset ([#] L)); :: thesis: for M being subnet of a_net F holds lim_inf F = lim_inf M
let M be subnet of a_net F; :: thesis: lim_inf F = lim_inf M
A1: lim_inf F = lim_inf (a_net F) by Th13;
for p being greater_or_equal_to_id Function of (a_net F),(a_net F) holds lim_inf F >= inf ((a_net F) * p) by Th15;
hence lim_inf F = lim_inf M by A1, WAYBEL28:15; :: thesis: verum