let L be complete LATTICE; :: thesis: for N being net of L

for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

let N be net of L; :: thesis: for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

let x be Element of L; :: thesis: ( N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) ) )

assume A1: N in NetUniv L ; :: thesis: ( ex M being subnet of N st

( M in NetUniv L & not x = lim_inf M ) or ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) ) )

assume A2: for M being subnet of N st M in NetUniv L holds

x = lim_inf M ; :: thesis: ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

N is subnet of N by YELLOW_6:14;

hence x = lim_inf N by A1, A2; :: thesis: for M being subnet of N st M in NetUniv L holds

x >= inf M

let M be subnet of N; :: thesis: ( M in NetUniv L implies x >= inf M )

assume M in NetUniv L ; :: thesis: x >= inf M

then x = lim_inf M by A2;

hence x >= inf M by Th1; :: thesis: verum

for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

let N be net of L; :: thesis: for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

let x be Element of L; :: thesis: ( N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds

x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) ) )

assume A1: N in NetUniv L ; :: thesis: ( ex M being subnet of N st

( M in NetUniv L & not x = lim_inf M ) or ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) ) )

assume A2: for M being subnet of N st M in NetUniv L holds

x = lim_inf M ; :: thesis: ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds

x >= inf M ) )

N is subnet of N by YELLOW_6:14;

hence x = lim_inf N by A1, A2; :: thesis: for M being subnet of N st M in NetUniv L holds

x >= inf M

let M be subnet of N; :: thesis: ( M in NetUniv L implies x >= inf M )

assume M in NetUniv L ; :: thesis: x >= inf M

then x = lim_inf M by A2;

hence x >= inf M by Th1; :: thesis: verum