let L be continuous complete LATTICE; :: thesis:
let N be net of L; :: according to YELLOW_6:def 22 :: thesis:
let x be Element of L; :: thesis:
assume that
A1: N in NetUniv L and
A2: not [N,x] in lim_inf-Convergence L ; :: thesis:
A3: ex N1 being strict net of L st
( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by A1, YELLOW_6:def 11;
not for M being subnet of N holds x = lim_inf M by A1, A2, Def3;
then A4: ( not x = lim_inf N or ex p being greater_or_equal_to_id Function of N,N st not x >= inf (N * p) ) by Th14;
A5: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def 18;

per cases by A1, A4, Th10;

suppose A6: ( not x = lim_inf N & x <= lim_inf N ) ; :: thesis:

reconsider N9 = N as subnet of N by YELLOW_6:14;
take N9 ; :: thesis:
thus N9 in NetUniv L by A1; :: thesis:
given M2 being subnet of N9 such that A7: [M2,x] in lim_inf-Convergence L ; :: thesis:
A8: lim_inf N <= lim_inf M2 by WAYBEL21:37;
A9: M2 is subnet of M2 by YELLOW_6:14;
M2 in NetUniv L by A5, A7, ZFMISC_1:87;
then lim_inf M2 = x by A7, A9, Def3;
hence contradiction by A6, A8, YELLOW_0:def 3; :: thesis:

end;

suppose ( not x = lim_inf N & not x <= lim_inf N ) ; :: thesis:

then not x is_S-limit_of N ;
then not [N,x] in Scott-Convergence L by A1, A3, WAYBEL11:def 8;
then consider M being subnet of N such that
A10: M in NetUniv L and
A11: for M1 being subnet of M holds not [M1,x] in Scott-Convergence L by A1, YELLOW_6:def 22;
take M ; :: thesis:
thus M in NetUniv L by A10; :: thesis:
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

let M1 be subnet of M; :: thesis:
A12: not [M1,x] in Scott-Convergence L by A11;
assume A13: [M1,x] in lim_inf-Convergence L ; :: thesis:
then A14: M1 in NetUniv L by A5, ZFMISC_1:87;
then ex M11 being strict net of L st
( M11 = M1 & the carrier of M11 in the_universe_of the carrier of L ) by YELLOW_6:def 11;
then A15: not x is_S-limit_of M1 by A14, A12, WAYBEL11:def 8;
M1 is subnet of M1 by YELLOW_6:14;
then x = lim_inf M1 by A13, A14, Def3;
hence contradiction by A15; :: thesis:

end;

hence for b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L ; :: thesis:

end;

suppose ex M being subnet of N st
( M in NetUniv L & not x >= inf M ) ; :: thesis:

then consider M being subnet of N such that
A16: M in NetUniv L and
A17: not x >= inf M ;
take M ; :: thesis:
thus M in NetUniv L by A16; :: thesis:
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

let M1 be subnet of M; :: thesis:
A18: M1 is subnet of M1 by YELLOW_6:14;
A19: ( lim_inf M1 >= lim_inf M & lim_inf M >= inf M ) by Th1, WAYBEL21:37;
assume A20: [M1,x] in lim_inf-Convergence L ; :: thesis:
then M1 in NetUniv L by A5, ZFMISC_1:87;
then x = lim_inf M1 by A20, A18, Def3;
hence contradiction by A17, A19, YELLOW_0:def 2; :: thesis:

end;

hence for b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L ; :: thesis:

end;

end;