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: [N,x] in lim_inf-Convergence L

then for M being subnet of N st M in NetUniv L holds

x >= inf M by A1, Th3;

then A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) by A1, Th10;

x = lim_inf N by A1, A2, Th3;

then for M being subnet of N holds x = lim_inf M by A3, Th14;

hence [N,x] in lim_inf-Convergence L by A1, Def3; :: thesis: verum

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: [N,x] in lim_inf-Convergence L

then for M being subnet of N st M in NetUniv L holds

x >= inf M by A1, Th3;

then A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) by A1, Th10;

x = lim_inf N by A1, A2, Th3;

then for M being subnet of N holds x = lim_inf M by A3, Th14;

hence [N,x] in lim_inf-Convergence L by A1, Def3; :: thesis: verum