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 7;
A2: incl (M,N) = id the carrier of M by WAYBEL_9:13, YELLOW_9:def 1;

now :: thesis: for k being Element of N
for j being Element of M st e . j <= k holds
ex k9 being Element of M st
( k9 >= j & N . k >= M . k9 )

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

end;

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