let L be continuous complete LATTICE; :: thesis: lim_inf-Convergence L is (DIVERGENCE)
let N be net of L; :: according to YELLOW_6:def 25 :: 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 A1: ( N in NetUniv L & 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 ) )
then not for M being subnet of N holds x = lim_inf M by Def3;
then A2: ( 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 Th15;
A3: lim_inf-Convergence L c= [:(NetUniv L),the carrier of L:] by YELLOW_6:def 21;
consider N1 being strict net of L such that
A4: N1 = N and
the carrier of N1 in the_universe_of the carrier of L by A1, YELLOW_6:def 14;

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, A2, Th11;

suppose A5: ( 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 N' = N as subnet of N by YELLOW_6:23;
take N' ; :: thesis: ( N' in NetUniv L & ( for b₁ being subnet of N' holds not [b₁,x] in lim_inf-Convergence L ) )
thus N' in NetUniv L by A1; :: thesis: for b₁ being subnet of N' holds not [b₁,x] in lim_inf-Convergence L
given M2 being subnet of N' such that A6: [M2,x] in lim_inf-Convergence L ; :: thesis: contradiction
A7: M2 in NetUniv L by A3, A6, ZFMISC_1:106;
M2 is subnet of M2 by YELLOW_6:23;
then A8: lim_inf M2 = x by A6, A7, Def3;
lim_inf N <= lim_inf M2 by WAYBEL21:37;
hence contradiction by A5, 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 by WAYBEL11:def 7;
then not [N,x] in Scott-Convergence L by A1, A4, WAYBEL11:def 8;
then consider M being subnet of N such that
A9: M in NetUniv L and
A10: for M1 being subnet of M holds not [M1,x] in Scott-Convergence L by A1, YELLOW_6:def 25;
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 A9; :: 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
assume A11: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction
then A12: M1 in NetUniv L by A3, ZFMISC_1:106;
then consider M11 being strict net of L such that
A13: M11 = M1 and
the carrier of M11 in the_universe_of the carrier of L by YELLOW_6:def 14;
M1 is subnet of M1 by YELLOW_6:23;
then A14: x = lim_inf M1 by A11, A12, Def3;
not [M1,x] in Scott-Convergence L by A10;
then not x is_S-limit_of M1 by A12, A13, WAYBEL11:def 8;
hence contradiction by A14, WAYBEL11:def 7; :: thesis: verum

end;

hence for M1 being subnet of M holds not [M1,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
A15: M in NetUniv L and
A16: 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 A15; :: 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
assume A17: [M1,x] in lim_inf-Convergence L ; :: thesis: contradiction
then A18: M1 in NetUniv L by A3, ZFMISC_1:106;
M1 is subnet of M1 by YELLOW_6:23;
then A19: x = lim_inf M1 by A17, A18, Def3;
A20: lim_inf M1 >= lim_inf M by WAYBEL21:37;
lim_inf M >= inf M by Th1;
hence contradiction by A16, A19, A20, YELLOW_0:def 2; :: thesis: verum

end;

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

end;

end;