let T be complete LATTICE; :: thesis:
let N be net of T; :: thesis:
let i be Element of N; :: thesis:
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:

let k be Element of N; :: thesis:
let j be Element of M; :: thesis:
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:
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:
thus k9 >= j by A1, A3, A5, YELLOW_0:60; :: thesis:
A6: M . k9 = N . (e . k9) by Th36;
M . k9 <= M . k9 ;
hence N . k >= M . k9 by A2, A6; :: thesis:

end;

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