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
( lim_inf F = lim_inf (a_net F) & ( 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 Th13, Th15;
hence lim_inf F = lim_inf M by WAYBEL28:14; :: thesis: verum