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