let T be complete LATTICE; :: thesis: for N being net of T
for i being Element of N holds lim_inf (N | i) = lim_inf N
let N be net of T; :: thesis: for i being Element of N holds lim_inf (N | i) = lim_inf N
let i be Element of N; :: thesis: lim_inf (N | i) = lim_inf N
reconsider M = N | i as subnet of N ;
reconsider e = incl M,N as Embedding of M,N by Th40;
M is full SubNetStr of N by WAYBEL_9:14;
then A1: M is full SubRelStr of N by YELLOW_6:def 9;
A2: incl M,N = id the carrier of M by WAYBEL_9:13, YELLOW_9:def 1;

now

let k be Element of N; :: thesis: for j being Element of M st e . j <= k holds
ex k' being Element of M st
( k' >= j & N . k >= M . k' )
let j be Element of M; :: thesis: ( e . j <= k implies ex k' being Element of M st
( k' >= j & N . k >= M . k' ) )
consider j' being Element of N such that
A3: ( j' = j & j' >= i ) by WAYBEL_9:def 7;
assume e . j <= k ; :: thesis: ex k' being Element of M st
( k' >= j & N . k >= M . k' )
then A4: k >= j' by A2, A3, FUNCT_1:35;
then k >= i by A3, YELLOW_0:def 2;
then reconsider k' = k as Element of M by WAYBEL_9:def 7;
take k' = k'; :: thesis: ( k' >= j & N . k >= M . k' )
thus k' >= j by A1, A3, A4, YELLOW_0:61; :: thesis: N . k >= M . k'
( M . k' = N . (e . k') & M . k' <= M . k' ) by Th36;
hence N . k >= M . k' by A2, FUNCT_1:35; :: thesis: verum

end;

hence lim_inf (N | i) = lim_inf N by Th38; :: thesis: verum