let L be complete LATTICE; :: thesis: lim_inf-Convergence L is (CONSTANTS)
let N be constant net of L; :: according to YELLOW_6:def 20 :: thesis: ( not N in NetUniv L or [N,(the_value_of N)] in lim_inf-Convergence L )
A1: for M being subnet of N holds the_value_of N = lim_inf M
proof
let M be subnet of N; :: thesis: the_value_of N = lim_inf M
A2: M is constant by Th16;
thus the_value_of N = the_value_of M by Th16
.= lim_inf M by A2, WAYBEL11:23 ; :: thesis: verum
end;
assume N in NetUniv L ; :: thesis: [N,(the_value_of N)] in lim_inf-Convergence L
hence [N,(the_value_of N)] in lim_inf-Convergence L by A1, Def3; :: thesis: verum