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

end;

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