:: WAYBEL28 semantic presentation

begin

theorem Th1: :: WAYBEL28:1
for L being complete LATTICE
for N being net of L holds inf N <= lim_inf N
proof
let L be complete LATTICE; ::_thesis: for N being net of L holds inf N <= lim_inf N
let N be net of L; ::_thesis: inf N <= lim_inf N
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L)) where j1 is Element of N : verum  }  ;
  {  ("/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L)) where j1 is Element of N : verum  }  c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L)) where j1 is Element of N : verum  }  or x in the carrier of L )
assume  x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L)) where j1 is Element of N : verum  }  ; ::_thesis: x in the carrier of L
then  ex j1 being Element of N st x = "/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
then reconsider X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,L)) where j1 is Element of N : verum  }  as Subset of L ;
set j = the Element of N;
A1:  {  (N . i) where i is Element of N : i >= the Element of N  }  c= rng the mapping of N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (N . i) where i is Element of N : i >= the Element of N  }  or x in rng the mapping of N )
A2: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
assume  x in  {  (N . i) where i is Element of N : i >= the Element of N  }  ; ::_thesis: x in rng the mapping of N
then consider i being Element of N such that
A3: x = N . i and
 i >= the Element of N ;
 x = the mapping of N . i by A3, WAYBEL_0:def_8;
hence  x in rng the mapping of N by A2, FUNCT_1:def_3; ::_thesis: verum
end;
reconsider X = X as Subset of L ;
set x = "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L);
 ( ex_inf_of  {  (N . i) where i is Element of N : i >= the Element of N  }  ,L & ex_inf_of rng the mapping of N,L ) by YELLOW_0:17;
then  "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L) >= "/\" ((rng the mapping of N),L) by A1, YELLOW_0:35;
then  "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L) >= Inf by YELLOW_2:def_6;
then A4: inf N <= "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L) by WAYBEL_9:def_2;
 ex_sup_of X,L by YELLOW_0:17;
then  ( "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L) in X & X is_<=_than "\/" (X,L) ) by YELLOW_0:def_9;
then  "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,L) <= "\/" (X,L) by LATTICE3:def_9;
hence  inf N <= lim_inf N by A4, YELLOW_0:def_2; ::_thesis: verum
end;

theorem :: WAYBEL28:2
for L being complete LATTICE
for N being net of L
for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )
proof
let L be complete LATTICE; ::_thesis: for N being net of L
for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )
let N be net of L; ::_thesis: for x being Element of L st ( for M being subnet of N holds x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )
let x be Element of L; ::_thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) ) )
assume A1: for M being subnet of N holds x = lim_inf M ; ::_thesis: ( x = lim_inf N & ( for M being subnet of N holds x >= inf M ) )
 N is subnet of N by YELLOW_6:14;
hence  x = lim_inf N by A1; ::_thesis: for M being subnet of N holds x >= inf M
let M be subnet of N; ::_thesis: x >= inf M
 x = lim_inf M by A1;
hence  x >= inf M by Th1; ::_thesis: verum
end;

theorem Th3: :: WAYBEL28:3
for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
proof
let L be complete LATTICE; ::_thesis: for N being net of L
for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
let N be net of L; ::_thesis: for x being Element of L st N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) holds
( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
let x be Element of L; ::_thesis: ( N in NetUniv L & ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) implies ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) ) )
assume A1: N in NetUniv L ; ::_thesis: ( ex M being subnet of N st
( M in NetUniv L & not x = lim_inf M ) or ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) ) )
assume A2: for M being subnet of N st M in NetUniv L holds
x = lim_inf M ; ::_thesis: ( x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) )
 N is subnet of N by YELLOW_6:14;
hence  x = lim_inf N by A1, A2; ::_thesis: for M being subnet of N st M in NetUniv L holds
x >= inf M
let M be subnet of N; ::_thesis: ( M in NetUniv L implies x >= inf M )
assume  M in NetUniv L ; ::_thesis: x >= inf M
then  x = lim_inf M by A2;
hence  x >= inf M by Th1; ::_thesis: verum
end;

definition
let N be non empty RelStr ;
let f be Function of N,N;
attrf is greater_or_equal_to_id  means :Def1: :: WAYBEL28:def 1
 for j being Element of N holds j <= f . j;
end;

:: deftheorem Def1 defines greater_or_equal_to_id WAYBEL28:def_1_:_
 for N being non empty RelStr
for f being Function of N,N holds
( f is greater_or_equal_to_id iff for j being Element of N holds j <= f . j );

theorem Th4: :: WAYBEL28:4
for N being non empty reflexive RelStr holds id N is greater_or_equal_to_id
proof
let N be non empty reflexive RelStr ; ::_thesis: id N is greater_or_equal_to_id
let j be Element of N; :: according to WAYBEL28:def_1 ::_thesis: j <= (id N) . j
reconsider n = j as Element of N ;
 n <= (id N) . n by FUNCT_1:18;
hence  j <= (id N) . j ; ::_thesis: verum
end;

theorem Th5: :: WAYBEL28:5
for N being non empty directed RelStr
for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )
proof
let N be non empty directed RelStr ; ::_thesis: for x, y being Element of N ex z being Element of N st
( x <= z & y <= z )
let x, y be Element of N; ::_thesis: ex z being Element of N st
( x <= z & y <= z )
 [#] N is directed by WAYBEL_0:def_6;
then  ex z being Element of N st
( z in [#] N & x <= z & y <= z ) by WAYBEL_0:def_1;
hence  ex z being Element of N st
( x <= z & y <= z ) ; ::_thesis: verum
end;

registration
let N be non empty directed RelStr ;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];
existence
 ex b1 being Function of N,N st b1 is greater_or_equal_to_id
proof
defpred S1[ set , set ] means  for n, m being Element of N st N = n & c2 = m holds
n <= m;
A1: for e being set st e in the carrier of N holds
ex u being set st
( u in the carrier of N & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier of N implies ex u being set st
( u in the carrier of N & S1[e,u] ) )
assume  e in the carrier of N ; ::_thesis: ex u being set st
( u in the carrier of N & S1[e,u] )
then reconsider e9 = e as Element of N ;
consider u9 being Element of N such that
A2: e9 <= u9 and
 e9 <= u9 by Th5;
take  u9 ; ::_thesis: ( u9 in the carrier of N & S1[e,u9] )
thus  u9 in the carrier of N ; ::_thesis: S1[e,u9]
let n, m be Element of N; ::_thesis: ( e = n & u9 = m implies n <= m )
assume  ( e = n & u9 = m ) ; ::_thesis: n <= m
hence  n <= m by A2; ::_thesis: verum
end;
consider p being Function such that
A3: ( dom p = the carrier of N & rng p c= the carrier of N ) and
A4: for e being set st e in the carrier of N holds
S1[e,p . e] from FUNCT_1:sch_5(A1);
reconsider p = p as Function of N,N by A3, FUNCT_2:2;
take  p ; ::_thesis: p is greater_or_equal_to_id
let j be Element of N; :: according to WAYBEL28:def_1 ::_thesis: j <= p . j
thus  j <= p . j by A4; ::_thesis: verum
end;
end;

registration
let N be non empty reflexive RelStr ;
cluster non empty Relation-like the carrier of N -defined the carrier of N -valued Function-like V34( the carrier of N) V35( the carrier of N, the carrier of N) greater_or_equal_to_id for Element of bool [: the carrier of N, the carrier of N:];
existence
 ex b1 being Function of N,N st b1 is greater_or_equal_to_id
proof
take  id N ; ::_thesis: id N is greater_or_equal_to_id
thus  id N is greater_or_equal_to_id by Th4; ::_thesis: verum
end;
end;

definition
let L be non empty 1-sorted ;
let N be non empty NetStr over L;
let f be Function of N,N;
funcN * f ->  non empty strict NetStr over L means :Def2: :: WAYBEL28:def 2
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of it = the mapping of N * f );
existence
 ex b1 being non empty strict NetStr over L st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f )
proof
take  NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) ; ::_thesis: ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) = the mapping of N * f )
thus  ( RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) = the mapping of N * f ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict NetStr over L st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b1 = the mapping of N * f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b2 = the mapping of N * f holds
b1 = b2 ;
end;

:: deftheorem Def2 defines * WAYBEL28:def_2_:_
 for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N
for b4 being non empty strict NetStr over L holds
( b4 = N * f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of N, the InternalRel of N #) & the mapping of b4 = the mapping of N * f ) );

theorem Th6: :: WAYBEL28:6
for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N holds the carrier of (N * f) = the carrier of N
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for f being Function of N,N holds the carrier of (N * f) = the carrier of N
let N be non empty NetStr over L; ::_thesis: for f being Function of N,N holds the carrier of (N * f) = the carrier of N
let f be Function of N,N; ::_thesis: the carrier of (N * f) = the carrier of N
 RelStr(# the carrier of (N * f), the InternalRel of (N * f) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2;
hence  the carrier of (N * f) = the carrier of N ; ::_thesis: verum
end;

theorem Th7: :: WAYBEL28:7
for L being non empty 1-sorted
for N being non empty NetStr over L
for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L
for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
let N be non empty NetStr over L; ::_thesis: for f being Function of N,N holds N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
let f be Function of N,N; ::_thesis: N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #)
 RelStr(# the carrier of (N * f), the InternalRel of (N * f) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2;
hence  N * f = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * f) #) by Def2; ::_thesis: verum
end;

theorem Th8: :: WAYBEL28:8
for L being non empty 1-sorted
for N being non empty transitive directed RelStr
for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty transitive directed RelStr
for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
let N be non empty transitive directed RelStr ; ::_thesis: for f being Function of the carrier of N, the carrier of L holds NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
let f be Function of the carrier of N, the carrier of L; ::_thesis: NetStr(# the carrier of N, the InternalRel of N,f #) is net of L
set N2 = NetStr(# the carrier of N, the InternalRel of N,f #);
A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of NetStr(# the carrier of N, the InternalRel of N,f #), the InternalRel of NetStr(# the carrier of N, the InternalRel of N,f #) #) ;
 [#] N is directed by WAYBEL_0:def_6;
then  [#] NetStr(# the carrier of N, the InternalRel of N,f #) is directed by A1, WAYBEL_0:3;
hence  NetStr(# the carrier of N, the InternalRel of N,f #) is net of L by A1, WAYBEL_0:def_6, WAYBEL_8:13; ::_thesis: verum
end;

registration
let L be non empty 1-sorted ;
let N be non empty transitive directed RelStr ;
let f be Function of the carrier of N, the carrier of L;
cluster NetStr(# the carrier of N, the InternalRel of N,f #) ->  non empty transitive directed ;
correctness
coherence
( NetStr(# the carrier of N, the InternalRel of N,f #) is transitive & NetStr(# the carrier of N, the InternalRel of N,f #) is directed & not NetStr(# the carrier of N, the InternalRel of N,f #) is empty );
by Th8;
end;

theorem Th9: :: WAYBEL28:9
for L being non empty 1-sorted
for N being net of L
for p being Function of N,N holds N * p is net of L
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for p being Function of N,N holds N * p is net of L
let N be net of L; ::_thesis: for p being Function of N,N holds N * p is net of L
let p be Function of N,N; ::_thesis: N * p is net of L
 N * p = NetStr(# the carrier of N, the InternalRel of N,( the mapping of N * p) #) by Th7;
hence  N * p is net of L ; ::_thesis: verum
end;

registration
let L be non empty 1-sorted ;
let N be net of L;
let p be Function of N,N;
clusterN * p ->  non empty transitive strict directed ;
correctness
coherence
( N * p is transitive & N * p is directed );
by Th9;
end;

theorem Th10: :: WAYBEL28:10
for L being non empty 1-sorted
for N being net of L
for p being Function of N,N st N in NetUniv L holds
N * p in NetUniv L
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for p being Function of N,N st N in NetUniv L holds
N * p in NetUniv L
let N be net of L; ::_thesis: for p being Function of N,N st N in NetUniv L holds
N * p in NetUniv L
let p be Function of N,N; ::_thesis: ( N in NetUniv L implies N * p in NetUniv L )
assume  N in NetUniv L ; ::_thesis: N * p in NetUniv L
then A1: ex N1 being strict net of L st
( N1 = N & the carrier of N1 in the_universe_of the carrier of L ) by YELLOW_6:def_11;
 the carrier of (N * p) = the carrier of N by Th6;
hence  N * p in NetUniv L by A1, YELLOW_6:def_11; ::_thesis: verum
end;

theorem :: WAYBEL28:11
for L being non empty 1-sorted
for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds
M is subnet of N
proof
let L be non empty 1-sorted ; ::_thesis: for N, M being net of L st NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) holds
M is subnet of N
let N, M be net of L; ::_thesis: ( NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) implies M is subnet of N )
assume A1: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = NetStr(# the carrier of M, the InternalRel of M, the mapping of M #) ; ::_thesis: M is subnet of N
A2: N is subnet of N by YELLOW_6:14;
 ex f being Function of M,N st
( the mapping of M = the mapping of N * f & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p ) )
proof
consider f being Function of N,N such that
A3: the mapping of N = the mapping of N * f and
A4: for m being Element of N ex n being Element of N st
for p being Element of N st n <= p holds
m <= f . p by A2, YELLOW_6:def_9;
reconsider f2 = f as Function of M,N by A1;
take  f2 ; ::_thesis: ( the mapping of M = the mapping of N * f2 & ( for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f2 . p ) )
thus  the mapping of M = the mapping of N * f2 by A1, A3; ::_thesis: for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f2 . p
let m be Element of N; ::_thesis: ex n being Element of M st
for p being Element of M st n <= p holds
m <= f2 . p
consider n being Element of N such that
A5: for p being Element of N st n <= p holds
m <= f . p by A4;
reconsider n2 = n as Element of M by A1;
take  n2 ; ::_thesis: for p being Element of M st n2 <= p holds
m <= f2 . p
let p be Element of M; ::_thesis: ( n2 <= p implies m <= f2 . p )
reconsider p1 = p as Element of N by A1;
assume  n2 <= p ; ::_thesis: m <= f2 . p
then  [n2,p] in the InternalRel of M by ORDERS_2:def_5;
then  n <= p1 by A1, ORDERS_2:def_5;
hence  m <= f2 . p by A5; ::_thesis: verum
end;
hence  M is subnet of N by YELLOW_6:def_9; ::_thesis: verum
end;

theorem Th12: :: WAYBEL28:12
for L being non empty 1-sorted
for N being net of L
for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
proof
let L be non empty 1-sorted ; ::_thesis: for N being net of L
for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
let N be net of L; ::_thesis: for p being greater_or_equal_to_id Function of N,N holds N * p is subnet of N
let p be greater_or_equal_to_id Function of N,N; ::_thesis: N * p is subnet of N
 ex f being Function of (N * p),N st
( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k ) )
proof
 the carrier of (N * p) = the carrier of N by Th6;
then reconsider f = p as Function of (N * p),N ;
take  f ; ::_thesis: ( the mapping of (N * p) = the mapping of N * f & ( for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k ) )
thus  the mapping of (N * p) = the mapping of N * f by Def2; ::_thesis: for m being Element of N ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k
let m be Element of N; ::_thesis: ex n being Element of (N * p) st
for k being Element of (N * p) st n <= k holds
m <= f . k
reconsider n = m as Element of (N * p) by Th6;
take  n ; ::_thesis: for k being Element of (N * p) st n <= k holds
m <= f . k
let k be Element of (N * p); ::_thesis: ( n <= k implies m <= f . k )
assume A1: n <= k ; ::_thesis: m <= f . k
reconsider k1 = k as Element of N by Th6;
A2: k1 <= p . k1 by Def1;
 RelStr(# the carrier of (N * p), the InternalRel of (N * p) #) = RelStr(# the carrier of N, the InternalRel of N #) by Def2;
then  m <= k1 by A1, YELLOW_0:1;
hence  m <= f . k by A2, YELLOW_0:def_2; ::_thesis: verum
end;
hence  N * p is subnet of N by YELLOW_6:def_9; ::_thesis: verum
end;

definition
let L be non empty 1-sorted ;
let N be net of L;
let p be greater_or_equal_to_id Function of N,N;
:: original: *
redefine funcN * p ->  strict subnet of N;
correctness
coherence
N * p is strict subnet of N;
by Th12;
end;

theorem :: WAYBEL28:13
for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L & x = lim_inf N & ( for M being subnet of N st M in NetUniv L holds
x >= inf M ) holds
( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) ) by Th10;

theorem Th14: :: WAYBEL28:14
for L being complete LATTICE
for N being net of L
for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
proof
let L be complete LATTICE; ::_thesis: for N being net of L
for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let N be net of L; ::_thesis: for x being Element of L st x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) holds
for M being subnet of N holds x = lim_inf M
let x be Element of L; ::_thesis: ( x = lim_inf N & ( for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ) implies for M being subnet of N holds x = lim_inf M )
assume that
A1: x = lim_inf N and
A2: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) ; ::_thesis: for M being subnet of N holds x = lim_inf M
let M be subnet of N; ::_thesis: x = lim_inf M
consider f being Function of M,N such that
A3: the mapping of M = the mapping of N * f and
A4: for j being Element of N ex k being Element of M st
for m being Element of M st k <= m holds
j <= f . m by YELLOW_6:def_9;
A5: x <= lim_inf M by A1, WAYBEL21:37;
A6: for k0 being Element of M holds "/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L) <= x
proof
let k0 be Element of M; ::_thesis: "/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L) <= x
defpred S1[ set , set ] means  for j being Element of N
for v, v9 being Element of M st $1 = j & $2 = v & v9 >= v holds
( v >= k0 & f . v9 >= j & f . v >= j );
A7: for j being Element of N ex v being Element of M st
( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )
proof
let j be Element of N; ::_thesis: ex v being Element of M st
( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )
consider w being Element of M such that
A8: for w9 being Element of M st w <= w9 holds
j <= f . w9 by A4;
consider v being Element of M such that
A9: v >= k0 and
A10: v >= w by Th5;
take  v ; ::_thesis: ( v >= k0 & ( for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j ) ) )
thus  v >= k0 by A9; ::_thesis: for v9 being Element of M st v9 >= v holds
( f . v9 >= j & f . v >= j )
let v9 be Element of M; ::_thesis: ( v9 >= v implies ( f . v9 >= j & f . v >= j ) )
assume  v9 >= v ; ::_thesis: ( f . v9 >= j & f . v >= j )
then  v9 >= w by A10, YELLOW_0:def_2;
hence  f . v9 >= j by A8; ::_thesis: f . v >= j
thus  f . v >= j by A8, A10; ::_thesis: verum
end;
A11: for e being set st e in the carrier of N holds
ex u being set st
( u in the carrier of M & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier of N implies ex u being set st
( u in the carrier of M & S1[e,u] ) )
assume  e in the carrier of N ; ::_thesis: ex u being set st
( u in the carrier of M & S1[e,u] )
then reconsider e9 = e as Element of N ;
consider u being Element of M such that
A12: u >= k0 and
A13: for v9 being Element of M st v9 >= u holds
( f . v9 >= e9 & f . u >= e9 ) by A7;
take  u ; ::_thesis: ( u in the carrier of M & S1[e,u] )
thus  u in the carrier of M ; ::_thesis: S1[e,u]
let j be Element of N; ::_thesis: for v, v9 being Element of M st e = j & u = v & v9 >= v holds
( v >= k0 & f . v9 >= j & f . v >= j )
let v, v9 be Element of M; ::_thesis: ( e = j & u = v & v9 >= v implies ( v >= k0 & f . v9 >= j & f . v >= j ) )
assume that
A14: e = j and
A15: u = v and
A16: v9 >= v ; ::_thesis: ( v >= k0 & f . v9 >= j & f . v >= j )
thus  v >= k0 by A12, A15; ::_thesis: ( f . v9 >= j & f . v >= j )
thus  f . v9 >= j by A13, A14, A15, A16; ::_thesis: f . v >= j
thus  f . v >= j by A13, A14, A15, A16; ::_thesis: verum
end;
consider g being Function such that
A17: dom g = the carrier of N and
A18: rng g c= the carrier of M and
A19: for e being set st e in the carrier of N holds
S1[e,g . e] from FUNCT_1:sch_5(A11);
reconsider g = g as Function of the carrier of N, the carrier of M by A17, A18, FUNCT_2:2;
A20: for j being Element of N holds g . j >= k0
proof
let j be Element of N; ::_thesis: g . j >= k0
reconsider v = g . j as Element of M ;
 ex v9 being Element of M st
( v9 >= v & v9 >= v ) by Th5;
hence  g . j >= k0 by A19; ::_thesis: verum
end;
reconsider g = g as Function of N,M ;
reconsider p = f * g as Function of N,N ;
 for j being Element of N holds j <= p . j
proof
let j be Element of N; ::_thesis: j <= p . j
reconsider v = g . j as Element of M ;
 [#] M is directed by WAYBEL_0:def_6;
then  ex v9 being Element of M st
( v9 in [#] M & v <= v9 & v <= v9 ) by WAYBEL_0:def_1;
then  j <= f . (g . j) by A19;
hence  j <= p . j by A17, FUNCT_1:13; ::_thesis: verum
end;
then reconsider p = p as greater_or_equal_to_id Function of N,N by Def1;
A21:  {  ((N * p) . j) where j is Element of (N * p) : verum  }  c=  {  (M . k) where k is Element of M : k >= k0  }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  or y in  {  (M . k) where k is Element of M : k >= k0  }  )
assume  y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  ; ::_thesis: y in  {  (M . k) where k is Element of M : k >= k0  }
then consider j being Element of (N * p) such that
A22: y = (N * p) . j ;
reconsider j9 = j as Element of N by Th6;
A23: the carrier of (N * p) = the carrier of N by Th6;
y = the mapping of (N * p) . j by A22, WAYBEL_0:def_8
.= ( the mapping of N * (f * g)) . j by Def2
.= ( the mapping of M * g) . j by A3, RELAT_1:36
.= the mapping of M . (g . j) by A17, A23, FUNCT_1:13 ;
then A24: y = M . (g . j9) by WAYBEL_0:def_8;
 g . j9 >= k0 by A20;
hence  y in  {  (M . k) where k is Element of M : k >= k0  }  by A24; ::_thesis: verum
end;
A25: ( ex_inf_of  {  ((N * p) . j) where j is Element of (N * p) : verum  }  ,L & ex_inf_of  {  (M . k) where k is Element of M : k >= k0  }  ,L ) by YELLOW_0:17;
A26: dom the mapping of (N * p) = the carrier of (N * p) by FUNCT_2:def_1;
A27: rng the mapping of (N * p) =  {  ((N * p) . j) where j is Element of (N * p) : verum  }
proof
thus  rng the mapping of (N * p) c=  {  ((N * p) . j) where j is Element of (N * p) : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ((N * p) . j) where j is Element of (N * p) : verum  }  c= rng the mapping of (N * p)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng the mapping of (N * p) or y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  )
assume  y in rng the mapping of (N * p) ; ::_thesis: y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }
then consider j1 being set  such that
A28: j1 in dom the mapping of (N * p) and
A29: the mapping of (N * p) . j1 = y by FUNCT_1:def_3;
reconsider j1 = j1 as Element of (N * p) by A28;
 y = (N * p) . j1 by A29, WAYBEL_0:def_8;
hence  y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  or y in rng the mapping of (N * p) )
assume  y in  {  ((N * p) . j) where j is Element of (N * p) : verum  }  ; ::_thesis: y in rng the mapping of (N * p)
then consider j being Element of (N * p) such that
A30: y = (N * p) . j ;
 y = the mapping of (N * p) . j by A30, WAYBEL_0:def_8;
hence  y in rng the mapping of (N * p) by A26, FUNCT_1:def_3; ::_thesis: verum
end;
A31: inf (N * p) <= x by A2;
inf (N * p) = Inf by WAYBEL_9:def_2
.= "/\" ( {  ((N * p) . j) where j is Element of (N * p) : verum  }  ,L) by A27, YELLOW_2:def_6 ;
then  "/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L) <= inf (N * p) by A25, A21, YELLOW_0:35;
hence  "/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L) <= x by A31, YELLOW_0:def_2; ::_thesis: verum
end;
 for b being Element of L st b in  {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  holds
b <= x
proof
let b be Element of L; ::_thesis: ( b in  {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  implies b <= x )
assume  b in  {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  ; ::_thesis: b <= x
then  ex k0 being Element of M st b = "/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L) ;
hence  b <= x by A6; ::_thesis: verum
end;
then A32: x is_>=_than  {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  by LATTICE3:def_9;
 ex_sup_of  {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  ,L by YELLOW_0:17;
then  "\/" ( {  ("/\" ( {  (M . k) where k is Element of M : k >= k0  }  ,L)) where k0 is Element of M : verum  }  ,L) <= x by A32, YELLOW_0:def_9;
hence  x = lim_inf M by A5, ORDERS_2:2; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
func lim_inf-Convergence L ->  Convergence-Class of L means :Def3: :: WAYBEL28:def 3
 for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in it iff for M being subnet of N holds x = lim_inf M );
existence
 ex b1 being Convergence-Class of L st
for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M )
proof
defpred S1[ set , set ] means  ex N being strict net of L st
( $1 = N & ( for M being subnet of N holds $2 = lim_inf M ) );
consider C being Relation of (NetUniv L), the carrier of L such that
A1: for N9 being Element of NetUniv L
for x being Element of L holds
( [N9,x] in C iff S1[N9,x] ) from RELSET_1:sch_2();
reconsider C = C as Convergence-Class of L by YELLOW_6:def_18;
take  C ; ::_thesis: for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C iff for M being subnet of N holds x = lim_inf M )
let N be net of L; ::_thesis: ( N in NetUniv L implies for x being Element of L holds
( [N,x] in C iff for M being subnet of N holds x = lim_inf M ) )
assume  N in NetUniv L ; ::_thesis: for x being Element of L holds
( [N,x] in C iff for M being subnet of N holds x = lim_inf M )
then reconsider N1 = N as Element of NetUniv L ;
let x be Element of L; ::_thesis: ( [N,x] in C iff for M being subnet of N holds x = lim_inf M )
thus  ( [N,x] in C implies for M being subnet of N holds x = lim_inf M ) ::_thesis: ( ( for M being subnet of N holds x = lim_inf M ) implies [N,x] in C )
proof
assume A2: [N,x] in C ; ::_thesis: for M being subnet of N holds x = lim_inf M
let M be subnet of N; ::_thesis: x = lim_inf M
 ex N2 being strict net of L st
( N1 = N2 & ( for M being subnet of N2 holds x = lim_inf M ) ) by A1, A2;
hence  x = lim_inf M ; ::_thesis: verum
end;
A3: ex N2 being strict net of L st
( N2 = N1 & the carrier of N2 in the_universe_of the carrier of L ) by YELLOW_6:def_11;
assume  for M being subnet of N holds x = lim_inf M ; ::_thesis: [N,x] in C
hence  [N,x] in C by A1, A3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Convergence-Class of L st ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b1 iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) ) holds
b1 = b2
proof
let C1, C2 be Convergence-Class of L; ::_thesis: ( ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M ) ) & ( for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M ) ) implies C1 = C2 )
assume that
A4: for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C1 iff for M being subnet of N holds x = lim_inf M ) and
A5: for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in C2 iff for M being subnet of N holds x = lim_inf M ) ; ::_thesis: C1 = C2
let Ns, xs be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [Ns,xs] in C1 or [Ns,xs] in C2 ) & ( not [Ns,xs] in C2 or [Ns,xs] in C1 ) )
A6: C1 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
thus  ( [Ns,xs] in C1 implies [Ns,xs] in C2 ) ::_thesis: ( not [Ns,xs] in C2 or [Ns,xs] in C1 )
proof
assume A7: [Ns,xs] in C1 ; ::_thesis: [Ns,xs] in C2
then reconsider x = xs as Element of L by A6, ZFMISC_1:87;
 Ns in NetUniv L by A6, A7, ZFMISC_1:87;
then consider N being strict net of L such that
A8: N = Ns and
 the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11;
A9: N in NetUniv L by A6, A7, A8, ZFMISC_1:87;
then  for M being subnet of N holds x = lim_inf M by A4, A7, A8;
hence  [Ns,xs] in C2 by A5, A8, A9; ::_thesis: verum
end;
assume A10: [Ns,xs] in C2 ; ::_thesis: [Ns,xs] in C1
A11: C2 c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then reconsider x = xs as Element of L by A10, ZFMISC_1:87;
 Ns in NetUniv L by A11, A10, ZFMISC_1:87;
then consider N being strict net of L such that
A12: N = Ns and
 the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11;
A13: N in NetUniv L by A11, A10, A12, ZFMISC_1:87;
then  for M being subnet of N holds x = lim_inf M by A5, A10, A12;
hence  [Ns,xs] in C1 by A4, A12, A13; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines lim_inf-Convergence WAYBEL28:def_3_:_
 for L being non empty RelStr
for b2 being Convergence-Class of L holds
( b2 = lim_inf-Convergence L iff for N being net of L st N in NetUniv L holds
for x being Element of L holds
( [N,x] in b2 iff for M being subnet of N holds x = lim_inf M ) );

theorem :: WAYBEL28:15
for L being complete LATTICE
for N being net of L
for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )
proof
let L be complete LATTICE; ::_thesis: for N being net of L
for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )
let N be net of L; ::_thesis: for x being Element of L st N in NetUniv L holds
( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )
let x be Element of L; ::_thesis: ( N in NetUniv L implies ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) )
assume A1: N in NetUniv L ; ::_thesis: ( [N,x] in lim_inf-Convergence L iff for M being subnet of N st M in NetUniv L holds
x = lim_inf M )
hence  ( [N,x] in lim_inf-Convergence L implies for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) by Def3; ::_thesis: ( ( for M being subnet of N st M in NetUniv L holds
x = lim_inf M ) implies [N,x] in lim_inf-Convergence L )
assume A2: for M being subnet of N st M in NetUniv L holds
x = lim_inf M ; ::_thesis: [N,x] in lim_inf-Convergence L
then  for M being subnet of N st M in NetUniv L holds
x >= inf M by A1, Th3;
then A3: for p being greater_or_equal_to_id Function of N,N holds x >= inf (N * p) by A1, Th10;
 x = lim_inf N by A1, A2, Th3;
then  for M being subnet of N holds x = lim_inf M by A3, Th14;
hence  [N,x] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum
end;

theorem Th16: :: WAYBEL28:16
for L being non empty RelStr
for N being constant net of L
for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )
proof
let L be non empty RelStr ; ::_thesis: for N being constant net of L
for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )
let N be constant net of L; ::_thesis: for M being subnet of N holds
( M is constant & the_value_of N = the_value_of M )
let M be subnet of N; ::_thesis: ( M is constant & the_value_of N = the_value_of M )
consider f being Function of M,N such that
A1: the mapping of M = the mapping of N * f and
 for m being Element of N ex n being Element of M st
for p being Element of M st n <= p holds
m <= f . p by YELLOW_6:def_9;
set y = the Element of dom the mapping of M;
A2: dom the mapping of N = the carrier of N by FUNCT_2:def_1;
then A3: the_value_of the mapping of N = the mapping of N . (f . the Element of dom the mapping of M) by FUNCT_1:def_12
.= the mapping of M . the Element of dom the mapping of M by A1, FUNCT_1:12 ;
A4: dom f = the carrier of M by FUNCT_2:def_1;
 for n1, n2 being set st n1 in dom the mapping of M & n2 in dom the mapping of M holds
the mapping of M . n1 = the mapping of M . n2
proof
let n1, n2 be set ; ::_thesis: ( n1 in dom the mapping of M & n2 in dom the mapping of M implies the mapping of M . n1 = the mapping of M . n2 )
assume that
A5: n1 in dom the mapping of M and
A6: n2 in dom the mapping of M ; ::_thesis: the mapping of M . n1 = the mapping of M . n2
A7: ( f . n1 in rng f & f . n2 in rng f ) by A4, A5, A6, FUNCT_1:def_3;
thus  the mapping of M . n1 = the mapping of N . (f . n1) by A1, A4, A5, FUNCT_1:13
.= the mapping of N . (f . n2) by A2, A7, FUNCT_1:def_10
.= the mapping of M . n2 by A1, A4, A6, FUNCT_1:13 ; ::_thesis: verum
end;
then A8: the mapping of M is constant by FUNCT_1:def_10;
hence A9: M is constant by YELLOW_6:def_4; ::_thesis: the_value_of N = the_value_of M
thus  the_value_of N = the_value_of the mapping of N by YELLOW_6:def_8
.= the_value_of the mapping of M by A8, A3, FUNCT_1:def_12
.= the_value_of M by A9, YELLOW_6:def_8 ; ::_thesis: verum
end;

definition
let L be non empty RelStr ;
func xi L ->  Subset-Family of L equals :: WAYBEL28:def 4
 the topology of (ConvergenceSpace (lim_inf-Convergence L));
correctness
coherence
the topology of (ConvergenceSpace (lim_inf-Convergence L)) is Subset-Family of L;
by YELLOW_6:def_24;
end;

:: deftheorem  defines xi WAYBEL28:def_4_:_
 for L being non empty RelStr holds xi L = the topology of (ConvergenceSpace (lim_inf-Convergence L));

theorem :: WAYBEL28:17
for L being complete LATTICE holds lim_inf-Convergence L is (CONSTANTS)
proof
let L be complete LATTICE; ::_thesis: lim_inf-Convergence L is (CONSTANTS)
let N be constant net of L; :: according to YELLOW_6:def_20 ::_thesis: ( not N in NetUniv L or [N,(the_value_of N)] in lim_inf-Convergence L )
A1: for M being subnet of N holds the_value_of N = lim_inf M
proof
let M be subnet of N; ::_thesis: the_value_of N = lim_inf M
A2: M is constant by Th16;
thus  the_value_of N = the_value_of M by Th16
.= lim_inf M by A2, WAYBEL11:23 ; ::_thesis: verum
end;
assume  N in NetUniv L ; ::_thesis: [N,(the_value_of N)] in lim_inf-Convergence L
hence  [N,(the_value_of N)] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum
end;

theorem :: WAYBEL28:18
for L being non empty RelStr holds lim_inf-Convergence L is (SUBNETS)
proof
let L be non empty RelStr ; ::_thesis: lim_inf-Convergence L is (SUBNETS)
let N be net of L; :: according to YELLOW_6:def_21 ::_thesis: for b1 being subnet of N holds
( not b1 in NetUniv L or for b2 being Element of the carrier of L holds
( not [N,b2] in lim_inf-Convergence L or [b1,b2] in lim_inf-Convergence L ) )
let M be subnet of N; ::_thesis: ( not M in NetUniv L or for b1 being Element of the carrier of L holds
( not [N,b1] in lim_inf-Convergence L or [M,b1] in lim_inf-Convergence L ) )
assume A1: M in NetUniv L ; ::_thesis: for b1 being Element of the carrier of L holds
( not [N,b1] in lim_inf-Convergence L or [M,b1] in lim_inf-Convergence L )
let x be Element of L; ::_thesis: ( not [N,x] in lim_inf-Convergence L or [M,x] in lim_inf-Convergence L )
assume A2: [N,x] in lim_inf-Convergence L ; ::_thesis: [M,x] in lim_inf-Convergence L
 lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then A3: N in NetUniv L by A2, ZFMISC_1:87;
 for M1 being subnet of M holds x = lim_inf M1
proof
let M1 be subnet of M; ::_thesis: x = lim_inf M1
reconsider M19 = M1 as subnet of N by YELLOW_6:15;
 x = lim_inf M19 by A2, A3, Def3;
hence  x = lim_inf M1 ; ::_thesis: verum
end;
hence  [M,x] in lim_inf-Convergence L by A1, Def3; ::_thesis: verum
end;

theorem :: WAYBEL28:19
for L being continuous complete LATTICE holds lim_inf-Convergence L is (DIVERGENCE)
proof
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 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 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;
percases ( ( 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;
supposeA6: ( 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 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 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 by WAYBEL11:def_7;
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 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
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, WAYBEL11:def_7; ::_thesis: verum
end;
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
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 b1 being subnet of M holds not [b1,x] in lim_inf-Convergence L ; ::_thesis: verum
end;
end;
end;

theorem :: WAYBEL28:20
for L being non empty RelStr
for N, x being set st [N,x] in lim_inf-Convergence L holds
N in NetUniv L
proof
let L be non empty RelStr ; ::_thesis: for N, x being set st [N,x] in lim_inf-Convergence L holds
N in NetUniv L
let N, x be set ; ::_thesis: ( [N,x] in lim_inf-Convergence L implies N in NetUniv L )
A1: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
assume  [N,x] in lim_inf-Convergence L ; ::_thesis: N in NetUniv L
hence  N in NetUniv L by A1, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th21: :: WAYBEL28:21
for L being non empty 1-sorted
for C1, C2 being Convergence-Class of L st C1 c= C2 holds
the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)
proof
let L be non empty 1-sorted ; ::_thesis: for C1, C2 being Convergence-Class of L st C1 c= C2 holds
the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)
let C1, C2 be Convergence-Class of L; ::_thesis: ( C1 c= C2 implies the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1) )
assume A1: C1 c= C2 ; ::_thesis: the topology of (ConvergenceSpace C2) c= the topology of (ConvergenceSpace C1)
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in the topology of (ConvergenceSpace C2) or A in the topology of (ConvergenceSpace C1) )
assume  A in the topology of (ConvergenceSpace C2) ; ::_thesis: A in the topology of (ConvergenceSpace C1)
then  A in  {  V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in C2 holds
N is_eventually_in V  }  by YELLOW_6:def_24;
then consider V1 being Subset of L such that
A2: A = V1 and
A3: for p being Element of L st p in V1 holds
for N being net of L st [N,p] in C2 holds
N is_eventually_in V1 ;
 ex V being Subset of L st
( A = V & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in C1 holds
N is_eventually_in V ) )
proof
take  V1 ; ::_thesis: ( A = V1 & ( for p being Element of L st p in V1 holds
for N being net of L st [N,p] in C1 holds
N is_eventually_in V1 ) )
thus  A = V1 by A2; ::_thesis: for p being Element of L st p in V1 holds
for N being net of L st [N,p] in C1 holds
N is_eventually_in V1
let p be Element of L; ::_thesis: ( p in V1 implies for N being net of L st [N,p] in C1 holds
N is_eventually_in V1 )
assume A4: p in V1 ; ::_thesis: for N being net of L st [N,p] in C1 holds
N is_eventually_in V1
let N be net of L; ::_thesis: ( [N,p] in C1 implies N is_eventually_in V1 )
assume  [N,p] in C1 ; ::_thesis: N is_eventually_in V1
hence  N is_eventually_in V1 by A1, A3, A4; ::_thesis: verum
end;
then  A in  {  V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in C1 holds
N is_eventually_in V  }  ;
hence  A in the topology of (ConvergenceSpace C1) by YELLOW_6:def_24; ::_thesis: verum
end;

theorem Th22: :: WAYBEL28:22
for L being non empty reflexive RelStr holds lim_inf-Convergence L c= Scott-Convergence L
proof
let L be non empty reflexive RelStr ; ::_thesis: lim_inf-Convergence L c= Scott-Convergence L
let Ns, xs be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [Ns,xs] in lim_inf-Convergence L or [Ns,xs] in Scott-Convergence L )
assume A1: [Ns,xs] in lim_inf-Convergence L ; ::_thesis: [Ns,xs] in Scott-Convergence L
A2: lim_inf-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then reconsider x = xs as Element of L by A1, ZFMISC_1:87;
 Ns in NetUniv L by A2, A1, ZFMISC_1:87;
then consider N being strict net of L such that
A3: N = Ns and
 the carrier of N in the_universe_of the carrier of L by YELLOW_6:def_11;
A4: N in NetUniv L by A2, A1, A3, ZFMISC_1:87;
 N is subnet of N by YELLOW_6:14;
then  x = lim_inf N by A1, A3, A4, Def3;
then  x is_S-limit_of N by WAYBEL11:def_7;
hence  [Ns,xs] in Scott-Convergence L by A3, A4, WAYBEL11:def_8; ::_thesis: verum
end;

theorem Th23: :: WAYBEL28:23
for X, Y being set st X c= Y holds
X in the_universe_of Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies X in the_universe_of Y )
A1: Y c= the_transitive-closure_of Y by CLASSES1:52;
 Tarski-Class (the_transitive-closure_of Y) is_Tarski-Class_of the_transitive-closure_of Y by CLASSES1:def_4;
then A2: the_transitive-closure_of Y in Tarski-Class (the_transitive-closure_of Y) by CLASSES1:def_3;
assume  X c= Y ; ::_thesis: X in the_universe_of Y
then  X c= the_transitive-closure_of Y by A1, XBOOLE_1:1;
hence  X in the_universe_of Y by A2, CLASSES1:def_1; ::_thesis: verum
end;

theorem Th24: :: WAYBEL28:24
for L being non empty reflexive transitive RelStr
for D being non empty directed Subset of L holds Net-Str D in NetUniv L
proof
let L be non empty reflexive transitive RelStr ; ::_thesis: for D being non empty directed Subset of L holds Net-Str D in NetUniv L
let D be non empty directed Subset of L; ::_thesis: Net-Str D in NetUniv L
 ( D in the_universe_of the carrier of L & the carrier of (Net-Str D) = D ) by Th23, WAYBEL21:32;
hence  Net-Str D in NetUniv L by YELLOW_6:def_11; ::_thesis: verum
end;

theorem Th25: :: WAYBEL28:25
for L being complete LATTICE
for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D
proof
let L be complete LATTICE; ::_thesis: for D being non empty directed Subset of L
for M being subnet of Net-Str D holds lim_inf M = sup D
let D be non empty directed Subset of L; ::_thesis: for M being subnet of Net-Str D holds lim_inf M = sup D
 for M being subnet of Net-Str D holds sup D >= inf M
proof
let M be subnet of Net-Str D; ::_thesis: sup D >= inf M
set i = the Element of M;
set f = the mapping of M;
consider g being Function of M,(Net-Str D) such that
A1: the mapping of M = the mapping of (Net-Str D) * g and
 for m being Element of (Net-Str D) ex n being Element of M st
for p being Element of M st n <= p holds
m <= g . p by YELLOW_6:def_9;
A2: dom the mapping of M = the carrier of M by FUNCT_2:def_1;
then  the mapping of M . the Element of M in rng the mapping of M by FUNCT_1:def_3;
then A3: "/\" ((rng the mapping of M),L) <= the mapping of M . the Element of M by YELLOW_0:17, YELLOW_4:2;
 g . the Element of M in the carrier of (Net-Str D) ;
then A4: g . the Element of M in D by WAYBEL21:32;
then g . the Element of M = (id D) . (g . the Element of M) by FUNCT_1:18
.= the mapping of (Net-Str D) . (g . the Element of M) by WAYBEL21:32
.= the mapping of M . the Element of M by A1, A2, FUNCT_1:12 ;
then  the mapping of M . the Element of M <= sup D by A4, YELLOW_2:22;
then  sup D >= "/\" ((rng the mapping of M),L) by A3, YELLOW_0:def_2;
then  sup D >= Inf by YELLOW_2:def_6;
hence  sup D >= inf M by WAYBEL_9:def_2; ::_thesis: verum
end;
then  ( lim_inf (Net-Str D) = sup D & ( for p being greater_or_equal_to_id Function of (Net-Str D),(Net-Str D) holds sup D >= inf ((Net-Str D) * p) ) ) by WAYBEL17:10;
hence  for M being subnet of Net-Str D holds lim_inf M = sup D by Th14; ::_thesis: verum
end;

theorem Th26: :: WAYBEL28:26
for L being non empty complete LATTICE
for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L
proof
let L be non empty complete LATTICE; ::_thesis: for D being non empty directed Subset of L holds [(Net-Str D),(sup D)] in lim_inf-Convergence L
let D be non empty directed Subset of L; ::_thesis: [(Net-Str D),(sup D)] in lim_inf-Convergence L
 ( Net-Str D in NetUniv L & ( for M being subnet of Net-Str D holds lim_inf M = sup D ) ) by Th24, Th25;
hence  [(Net-Str D),(sup D)] in lim_inf-Convergence L by Def3; ::_thesis: verum
end;

theorem Th27: :: WAYBEL28:27
for L being complete LATTICE
for U1 being Subset of L st U1 in xi L holds
U1 is property(S)
proof
let L be complete LATTICE; ::_thesis: for U1 being Subset of L st U1 in xi L holds
U1 is property(S)
let U1 be Subset of L; ::_thesis: ( U1 in xi L implies U1 is property(S) )
assume  U1 in xi L ; ::_thesis: U1 is property(S)
then  U1 in  {  V where V is Subset of L : for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V  }  by YELLOW_6:def_24;
then A1: ex V being Subset of L st
( U1 = V & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in lim_inf-Convergence L holds
N is_eventually_in V ) ) ;
let D be non empty directed Subset of L; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,L) in U1 or ex b1 being Element of the carrier of L st
( b1 in D & ( for b2 being Element of the carrier of L holds
( not b2 in D or not b1 <= b2 or b2 in U1 ) ) ) )
assume A2: sup D in U1 ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in D & ( for b2 being Element of the carrier of L holds
( not b2 in D or not b1 <= b2 or b2 in U1 ) ) )
 [(Net-Str D),(sup D)] in lim_inf-Convergence L by Th26;
then  Net-Str D is_eventually_in U1 by A1, A2;
then consider y being Element of (Net-Str D) such that
A3: for x being Element of (Net-Str D) st y <= x holds
(Net-Str D) . x in U1 by WAYBEL_0:def_11;
A4: y in the carrier of (Net-Str D) ;
then  y in D by WAYBEL21:32;
then reconsider y1 = y as Element of L ;
reconsider y1 = y1 as Element of L ;
take  y1 ; ::_thesis: ( y1 in D & ( for b1 being Element of the carrier of L holds
( not b1 in D or not y1 <= b1 or b1 in U1 ) ) )
thus  y1 in D by A4, WAYBEL21:32; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 in D or not y1 <= b1 or b1 in U1 )
let x1 be Element of L; ::_thesis: ( not x1 in D or not y1 <= x1 or x1 in U1 )
assume that
A5: x1 in D and
A6: x1 >= y1 ; ::_thesis: x1 in U1
A7: Net-Str D is full SubRelStr of L by WAYBEL21:32;
reconsider x = x1 as Element of (Net-Str D) by A5, WAYBEL21:32;
reconsider x = x as Element of (Net-Str D) ;
(Net-Str D) . x = the mapping of (Net-Str D) . x by WAYBEL_0:def_8
.= (id D) . x by WAYBEL21:32
.= x by A5, FUNCT_1:18 ;
hence  x1 in U1 by A3, A6, A7, YELLOW_0:60; ::_thesis: verum
end;

theorem Th28: :: WAYBEL28:28
for L being non empty reflexive RelStr
for A being Subset of L st A in sigma L holds
A in xi L
proof
let L be non empty reflexive RelStr ; ::_thesis: for A being Subset of L st A in sigma L holds
A in xi L
let A be Subset of L; ::_thesis: ( A in sigma L implies A in xi L )
assume A1: A in sigma L ; ::_thesis: A in xi L
 the topology of (ConvergenceSpace (Scott-Convergence L)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by Th21, Th22;
hence  A in xi L by A1; ::_thesis: verum
end;

theorem Th29: :: WAYBEL28:29
for L being complete LATTICE
for A being Subset of L st A is upper & A in xi L holds
A in sigma L
proof
let L be complete LATTICE; ::_thesis: for A being Subset of L st A is upper & A in xi L holds
A in sigma L
let A be Subset of L; ::_thesis: ( A is upper & A in xi L implies A in sigma L )
set T = the Scott TopAugmentation of L;
A1: RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of the Scott TopAugmentation of L ;
reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ;
assume  A is upper ; ::_thesis: ( not A in xi L or A in sigma L )
then A2: A9 is upper by A1, WAYBEL_0:25;
assume  A in xi L ; ::_thesis: A in sigma L
then  A9 is property(S) by A1, Th27, YELLOW12:19;
then  A9 is open by A2, WAYBEL11:15;
then  A9 in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2;
hence  A in sigma L by YELLOW_9:51; ::_thesis: verum
end;

theorem :: WAYBEL28:30
for L being complete LATTICE
for A being Subset of L st A is lower holds
( A ` in xi L iff A is closed_under_directed_sups )
proof
let L be complete LATTICE; ::_thesis: for A being Subset of L st A is lower holds
( A ` in xi L iff A is closed_under_directed_sups )
let A be Subset of L; ::_thesis: ( A is lower implies ( A ` in xi L iff A is closed_under_directed_sups ) )
set T = the Scott TopAugmentation of L;
assume A1: A is lower ; ::_thesis: ( A ` in xi L iff A is closed_under_directed_sups )
then reconsider A1 = A as lower Subset of L ;
A2: RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of the Scott TopAugmentation of L, the InternalRel of the Scott TopAugmentation of L #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of the Scott TopAugmentation of L ;
reconsider A9 = A9 as Subset of the Scott TopAugmentation of L ;
A3: A1 ` is upper ;
thus  ( A ` in xi L implies A is closed_under_directed_sups ) ::_thesis: ( A is closed_under_directed_sups implies A ` in xi L )
proof
assume  A ` in xi L ; ::_thesis: A is closed_under_directed_sups
then  A9 ` in sigma L by A3, A2, Th29;
then  A9 ` in the topology of the Scott TopAugmentation of L by YELLOW_9:51;
then  A9 ` is open by PRE_TOPC:def_2;
then  A9 is closed by TOPS_1:3;
then  A9 is directly_closed by WAYBEL11:7;
hence  A is closed_under_directed_sups by A2, YELLOW12:20; ::_thesis: verum
end;
assume  A is closed_under_directed_sups ; ::_thesis: A ` in xi L
then A4: A9 is directly_closed by A2, YELLOW12:20;
 A9 is lower by A1, A2, WAYBEL_0:25;
then  A9 is closed by A4, WAYBEL11:7;
then  A9 ` is open by TOPS_1:3;
then  A9 ` in the topology of the Scott TopAugmentation of L by PRE_TOPC:def_2;
then  A ` in sigma L by A2, YELLOW_9:51;
hence  A ` in xi L by Th28; ::_thesis: verum
end;