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