let L be continuous complete LATTICE; :: thesis:
let N be net of L; :: according to YELLOW_6:def 22 :: thesis: for b1 being Element of the carrier of L holds
( not N in NetUniv L or [N,b1] in lim_inf-Convergence L or ex b2 being subnet of N st
( b2 in NetUniv L & ( for b3 being subnet of b2 holds not [b3,b1] in lim_inf-Convergence L ) ) )

let x be Element of L; :: thesis: ( not N in NetUniv L or [N,x] in lim_inf-Convergence L or ex b1 being subnet of N st
( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) ) )

assume that
A1: N in NetUniv L and
A2: not [N,x] in lim_inf-Convergence L ; :: thesis: ex b1 being subnet of N st
( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) )

A3: ex N1 being strict net of L st
( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by ;
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= [:(), the carrier of L:] by YELLOW_6:def 18;
per cases ( ( not x = lim_inf N & x <= lim_inf N ) or ( not x = lim_inf N & not x <= lim_inf N ) or ex M being subnet of N st
( M in NetUniv L & not x >= inf M ) )
by A1, A4, Th10;
suppose A6: ( not x = lim_inf N & x <= lim_inf N ) ; :: thesis: ex b1 being subnet of N st
( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) )

reconsider N9 = N as subnet of N by YELLOW_6:14;
take N9 ; :: thesis: ( N9 in NetUniv L & ( for b1 being subnet of N9 holds not [b1,x] in lim_inf-Convergence L ) )
thus N9 in NetUniv L by A1; :: thesis: for b1 being subnet of N9 holds not [b1,x] in lim_inf-Convergence L
given M2 being subnet of N9 such that A7: [M2,x] in lim_inf-Convergence L ; :: thesis: contradiction
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 ;
then lim_inf M2 = x by A7, A9, Def3;
hence contradiction by A6, A8, YELLOW_0:def 3; :: thesis: verum
end;
suppose ( not x = lim_inf N & not x <= lim_inf N ) ; :: thesis: ex b1 being subnet of N st
( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) )

then not x is_S-limit_of N ;
then not [N,x] in Scott-Convergence L by ;
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 ;
take M ; :: thesis: ( M in NetUniv L & ( for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ) )
thus M in NetUniv L by A10; :: thesis: for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L hence for b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ; :: thesis: verum
end;
suppose ex M being subnet of N st
( M in NetUniv L & not x >= inf M ) ; :: thesis: ex b1 being subnet of N st
( b1 in NetUniv L & ( for b2 being subnet of b1 holds not [b2,x] in lim_inf-Convergence L ) )

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