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