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

for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

let N be net of L; :: thesis: for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

let x be Element of L; :: thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) )

assume A1: for M being subnet of N holds x = lim_inf M ; :: thesis: ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

N is subnet of N by YELLOW_6:14;

hence x = lim_inf N by A1; :: thesis: for M being subnet of N holds x >= inf M

let M be subnet of N; :: thesis: x >= inf M

x = lim_inf M by A1;

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

for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

let N be net of L; :: thesis: for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds

( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

let x be Element of L; :: thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) )

assume A1: for M being subnet of N holds x = lim_inf M ; :: thesis: ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )

N is subnet of N by YELLOW_6:14;

hence x = lim_inf N by A1; :: thesis: for M being subnet of N holds x >= inf M

let M be subnet of N; :: thesis: x >= inf M

x = lim_inf M by A1;

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