let L be continuous complete LATTICE; :: thesis: lim_inf-Convergence L is (DIVERGENCE)
let N be net of L; :: according to YELLOW_6:def 22 :: thesis: for b₁ being Element of the carrier of L holds
( not N in NetUniv L or [N,b₁] in lim_inf-Convergence L or ex b₂ being subnet of N st
( b₂ in NetUniv L & ( for b₃ being subnet of b₂ holds not [b₃,b₁] 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 b₁ being subnet of N st
( b₁ in NetUniv L & ( for b₂ being subnet of b₁ holds not [b₂,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 b₁ being subnet of N st
( b₁ in NetUniv L & ( for b₂ being subnet of b₁ holds not [b₂,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 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 ( ( 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 b₁ being subnet of N st
( b₁ in NetUniv L & ( for b₂ being subnet of b₁ holds not [b₂,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 b₁ being subnet of N9 holds not [b₁,x] in lim_inf-Convergence L ) )
thus N9 in NetUniv L by A1; :: thesis: for b₁ being subnet of N9 holds not [b₁,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 A5, A7, ZFMISC_1:87;
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 b₁ being subnet of N st
( b₁ in NetUniv L & ( for b₂ being subnet of b₁ holds not [b₂,x] in lim_inf-Convergence L ) )

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: ( M in NetUniv L & ( for b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L ) )
thus M in NetUniv L by A10; :: thesis: for b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

proof

let M1 be subnet of M; :: thesis: not [M1,x] in lim_inf-Convergence L
A12: not [M1,x] in Scott-Convergence L by A11;
assume A13: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction
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: verum

end;

hence for b₁ being subnet of M holds not [b₁,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 b₁ being subnet of N st
( b₁ in NetUniv L & ( for b₂ being subnet of b₁ holds not [b₂,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 b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L ) )
thus M in NetUniv L by A16; :: thesis: for b₁ being subnet of M holds not [b₁,x] in lim_inf-Convergence L
for M1 being subnet of M holds not [M1,x] in lim_inf-Convergence L

proof

let M1 be subnet of M; :: thesis: not [M1,x] in lim_inf-Convergence L
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: contradiction
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: verum

end;

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

end;

end;