let L be complete LATTICE; :: thesis: for N being net of L
for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )

let N be net of L; :: thesis: for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )

let x be Element of L; :: thesis: ( N in NetUniv L implies ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) )

assume A1: N in NetUniv L ; :: thesis: ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )

hence ( [N,x] in lim_inf-Convergence L implies for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) by Def3; :: thesis: ( ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) implies [N,x] in lim_inf-Convergence L )

assume A2: for M being subnet of N st M in NetUniv L holds
x = lim_inf M ; :: thesis:
then for M being subnet of N st M in NetUniv L holds
x >= inf M by ;
then A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) by ;
x = lim_inf N by A1, A2, Th3;
then for M being subnet of N holds x = lim_inf M by ;
hence [N,x] in lim_inf-Convergence L by ; :: thesis: verum