:: WAYBEL32 semantic presentation

begin

definition
let T be non empty TopRelStr ;
attrT is upper  means :Def1: :: WAYBEL32:def 1
 {  ((downarrow x) `) where x is Element of T : verum  }  is prebasis of T;
end;

:: deftheorem Def1 defines upper WAYBEL32:def_1_:_
 for T being non empty TopRelStr holds
( T is upper iff  {  ((downarrow x) `) where x is Element of T : verum  }  is prebasis of T );

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict Scott for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is Scott & b1 is up-complete & b1 is strict )
proof
set R = the complete LATTICE;
set T = the correct strict Scott TopAugmentation of the complete LATTICE;
take  the correct strict Scott TopAugmentation of the complete LATTICE ; ::_thesis: ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict )
thus  ( the correct strict Scott TopAugmentation of the complete LATTICE is Scott & the correct strict Scott TopAugmentation of the complete LATTICE is up-complete & the correct strict Scott TopAugmentation of the complete LATTICE is strict ) ; ::_thesis: verum
end;
end;

definition
let T be non empty TopSpace-like reflexive TopRelStr ;
attrT is order_consistent  means :Def2: :: WAYBEL32:def 2
 for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) );
end;

:: deftheorem Def2 defines order_consistent WAYBEL32:def_2_:_
 for T being non empty TopSpace-like reflexive TopRelStr holds
( T is order_consistent iff for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) ) );

registration
cluster1 -element TopSpace-like reflexive  -> 1 -element TopSpace-like reflexive upper for TopRelStr ;
coherence
 for b1 being 1 -element TopSpace-like reflexive TopRelStr holds b1 is upper
proof
let T be 1 -element TopSpace-like reflexive TopRelStr ; ::_thesis: T is upper
set BB =  {  ((downarrow x) `) where x is Element of T : verum  }  ;
  {  ((downarrow x) `) where x is Element of T : verum  }  c= bool the carrier of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((downarrow x) `) where x is Element of T : verum  }  or a in bool the carrier of T )
assume  a in  {  ((downarrow x) `) where x is Element of T : verum  }  ; ::_thesis: a in bool the carrier of T
then  ex x being Element of T st a = (downarrow x) ` ;
hence  a in bool the carrier of T ; ::_thesis: verum
end;
then reconsider C =  {  ((downarrow x) `) where x is Element of T : verum  }  as Subset-Family of T ;
reconsider C = C as Subset-Family of T ;
A1:  {  ((downarrow x) `) where x is Element of T : verum  }  c= the topology of T
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((downarrow x) `) where x is Element of T : verum  }  or a in the topology of T )
assume  a in  {  ((downarrow x) `) where x is Element of T : verum  }  ; ::_thesis: a in the topology of T
then consider x being Element of T such that
A2: a = (downarrow x) ` ;
 a c= {}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in a or y in {} )
assume A3: y in a ; ::_thesis: y in {}
A4: x <= x ;
A5: y = x by A2, A3, STRUCT_0:def_10;
 x in downarrow x by A4, WAYBEL_0:17;
then A6: x in (downarrow x) /\ a by A3, A5, XBOOLE_0:def_4;
 downarrow x misses a by A2, XBOOLE_1:79;
hence  y in {} by A6, XBOOLE_0:def_7; ::_thesis: verum
end;
then  a = {} ;
hence  a in the topology of T by PRE_TOPC:1; ::_thesis: verum
end;
reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10;
  {  ((downarrow x) `) where x is Element of T : verum  }  = {{}}
proof
thus   {  ((downarrow x) `) where x is Element of T : verum  }  c= {{}} :: according to XBOOLE_0:def_10 ::_thesis: {{}} c=  {  ((downarrow x) `) where x is Element of T : verum  }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  ((downarrow x) `) where x is Element of T : verum  }  or a in {{}} )
assume  a in  {  ((downarrow x) `) where x is Element of T : verum  }  ; ::_thesis: a in {{}}
then consider x being Element of T such that
A7: a = (downarrow x) ` ;
A8: x <= x ;
A9: the carrier of T = {x} by YELLOW_9:9;
 x in downarrow x by A8, WAYBEL_0:17;
then  ( a = {} or ( a = the carrier of T & not x in a ) ) by A7, A9, XBOOLE_0:def_5, ZFMISC_1:33;
hence  a in {{}} by TARSKI:def_1; ::_thesis: verum
end;
set x = the Element of T;
A10: the Element of T <= the Element of T ;
A11: the carrier of T = { the Element of T} by YELLOW_9:9;
 the Element of T in downarrow the Element of T by A10, WAYBEL_0:17;
then  ( (downarrow the Element of T) ` = {} or ( (downarrow the Element of T) ` = the carrier of T & not the Element of T in (downarrow the Element of T) ` ) ) by A11, XBOOLE_0:def_5, ZFMISC_1:33;
then  {} in  {  ((downarrow x) `) where x is Element of T : verum  }  ;
hence  {{}} c=  {  ((downarrow x) `) where x is Element of T : verum  }  by ZFMISC_1:31; ::_thesis: verum
end;
then  FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then  F c= FinMeetCl C by ZFMISC_1:7;
hence   {  ((downarrow x) `) where x is Element of T : verum  }  is prebasis of T by A1, CANTOR_1:def_4, TOPS_2:64; :: according to WAYBEL32:def_1 ::_thesis: verum
end;
end;

registration
cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is upper & b1 is trivial & b1 is up-complete & b1 is strict )
proof
set T = the 1 -element up-complete strict TopLattice;
take  the 1 -element up-complete strict TopLattice ; ::_thesis: ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict )
thus  ( the 1 -element up-complete strict TopLattice is upper & the 1 -element up-complete strict TopLattice is trivial & the 1 -element up-complete strict TopLattice is up-complete & the 1 -element up-complete strict TopLattice is strict ) ; ::_thesis: verum
end;
end;

theorem Th1: :: WAYBEL32:1
for T being non empty up-complete upper TopPoset
for A being Subset of T st A is open holds
A is upper
proof
let T be non empty up-complete upper TopPoset; ::_thesis: for A being Subset of T st A is open holds
A is upper
let A be Subset of T; ::_thesis: ( A is open implies A is upper )
assume  A is open ; ::_thesis: A is upper
then A1: A in the topology of T by PRE_TOPC:def_2;
reconsider BB =  {  ((downarrow x) `) where x is Element of T : verum  }  as prebasis of T by Def1;
consider F being Basis of T such that
A2: F c= FinMeetCl BB by CANTOR_1:def_4;
 the topology of T c= UniCl F by CANTOR_1:def_2;
then consider Y being Subset-Family of T such that
A3: Y c= F and
A4: A = union Y by A1, CANTOR_1:def_1;
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume  x in A ; ::_thesis: ( not x <= y or y in A )
then consider Z being set  such that
A5: x in Z and
A6: Z in Y by A4, TARSKI:def_4;
 Z in F by A3, A6;
then consider X being Subset-Family of T such that
A7: X c= BB and
 X is finite and
A8: Z = Intersect X by A2, CANTOR_1:def_3;
assume A9: x <= y ; ::_thesis: y in A
now__::_thesis:_for_Q_being_set_st_Q_in_X_holds_
y_in_Q
let Q be set ; ::_thesis: ( Q in X implies y in Q )
assume A10: Q in X ; ::_thesis: y in Q
then  Q in BB by A7;
then consider z being Element of T such that
A11: Q = (downarrow z) ` ;
A12: x in Q by A5, A8, A10, SETFAM_1:43;
 downarrow z misses Q by A11, XBOOLE_1:79;
then  not x in downarrow z by A12, XBOOLE_0:3;
then  not x <= z by WAYBEL_0:17;
then  not y <= z by A9, ORDERS_2:3;
then  not y in downarrow z by WAYBEL_0:17;
hence  y in Q by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then  y in Z by A8, SETFAM_1:43;
hence  y in A by A4, A6, TARSKI:def_4; ::_thesis: verum
end;

theorem :: WAYBEL32:2
for T being non empty up-complete TopPoset st T is upper holds
T is order_consistent
proof
let T be non empty up-complete TopPoset; ::_thesis: ( T is upper implies T is order_consistent )
assume A1: T is upper ; ::_thesis: T is order_consistent
then reconsider BB =  {  ((downarrow x) `) where x is Element of T : verum  }  as prebasis of T by Def1;
 for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
A2: downarrow x c= Cl {x}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in Cl {x} )
assume A3: a in downarrow x ; ::_thesis: a in Cl {x}
then reconsider a9 = a as Point of T ;
 for G being Subset of T st G is open & a9 in G holds
{x} meets G
proof
let G be Subset of T; ::_thesis: ( G is open & a9 in G implies {x} meets G )
assume A4: G is open ; ::_thesis: ( not a9 in G or {x} meets G )
assume A5: a9 in G ; ::_thesis: {x} meets G
reconsider v = a9 as Element of T ;
A6: v <= x by A3, WAYBEL_0:17;
 G is upper by A1, A4, Th1;
then A7: x in G by A5, A6, WAYBEL_0:def_20;
 x in {x} by TARSKI:def_1;
hence  {x} meets G by A7, XBOOLE_0:3; ::_thesis: verum
end;
hence  a in Cl {x} by PRE_TOPC:24; ::_thesis: verum
end;
 Cl {x} c= downarrow x
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Cl {x} or a in downarrow x )
assume A8: a in Cl {x} ; ::_thesis: a in downarrow x
reconsider BB = BB as Subset-Family of T ;
 (downarrow x) ` in BB ;
then A9: (downarrow x) ` is open by TOPS_2:def_1;
 (downarrow x) ` = ([#] T) \ (downarrow x) ;
then A10: downarrow x is closed by A9, PRE_TOPC:def_3;
 x <= x ;
then  x in downarrow x by WAYBEL_0:17;
then  {x} c= downarrow x by ZFMISC_1:31;
hence  a in downarrow x by A8, A10, PRE_TOPC:15; ::_thesis: verum
end;
hence  downarrow x = Cl {x} by A2, XBOOLE_0:def_10; ::_thesis: for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
thus  for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ::_thesis: verum
proof
let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume  x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V
then A11: x = Sup by WAYBEL_2:def_1
.= sup (rng (netmap (N,T))) by YELLOW_2:def_5 ;
let V be a_neighborhood of x; ::_thesis: N is_eventually_in V
A12: x in Int V by CONNSP_2:def_1;
 FinMeetCl BB is Basis of T by YELLOW_9:23;
then A13: the topology of T = UniCl (FinMeetCl BB) by YELLOW_9:22;
 Int V in the topology of T by PRE_TOPC:def_2;
then consider Y being Subset-Family of T such that
A14: Y c= FinMeetCl BB and
A15: Int V = union Y by A13, CANTOR_1:def_1;
consider Y1 being set  such that
A16: x in Y1 and
A17: Y1 in Y by A12, A15, TARSKI:def_4;
consider Z being Subset-Family of T such that
A18: Z c= BB and
A19: Z is finite and
A20: Y1 = Intersect Z by A14, A17, CANTOR_1:def_3;
reconsider rngN = rng (netmap (N,T)) as Subset of T ;
 rngN is directed by WAYBEL_2:18;
then  ex a being Element of T st
( a is_>=_than rngN & ( for b being Element of T st b is_>=_than rngN holds
a <= b ) ) by WAYBEL_0:def_39;
then A21: ex_sup_of rngN,T by YELLOW_0:15;
defpred S1[ set , set ] means  for i, j being Element of N st i = $2 & j >= i holds
N . j in $1;
A22: for Q being set st Q in Z holds
ex b being set st
( b in the carrier of N & S1[Q,b] )
proof
let Q be set ; ::_thesis: ( Q in Z implies ex b being set st
( b in the carrier of N & S1[Q,b] ) )
assume A23: Q in Z ; ::_thesis: ex b being set st
( b in the carrier of N & S1[Q,b] )
then  Q in BB by A18;
then consider v1 being Element of T such that
A24: Q = (downarrow v1) ` ;
 x in (downarrow v1) ` by A16, A20, A23, A24, SETFAM_1:43;
then  not x in downarrow v1 by XBOOLE_0:def_5;
then A25: not x <= v1 by WAYBEL_0:17;
 not rngN c= downarrow v1
proof
assume A26: rngN c= downarrow v1 ; ::_thesis: contradiction
 ex_sup_of downarrow v1,T by WAYBEL_0:34;
then  sup rngN <= sup (downarrow v1) by A21, A26, YELLOW_0:34;
hence  contradiction by A11, A25, WAYBEL_0:34; ::_thesis: verum
end;
then consider w being set  such that
A27: w in rngN and
A28: not w in downarrow v1 by TARSKI:def_3;
reconsider w9 = w as Element of T by A27;
consider i being set  such that
A29: i in dom the mapping of N and
A30: w9 = the mapping of N . i by A27, FUNCT_1:def_3;
reconsider i = i as Element of N by A29;
consider b being Element of N such that
A31: for l being Element of N st b <= l holds
N . i <= N . l by WAYBEL_0:11;
take  b ; ::_thesis: ( b in the carrier of N & S1[Q,b] )
thus  b in the carrier of N ; ::_thesis: S1[Q,b]
thus  for j, k being Element of N st j = b & k >= j holds
N . k in Q ::_thesis: verum
proof
let j, k be Element of N; ::_thesis: ( j = b & k >= j implies N . k in Q )
assume that
A32: j = b and
A33: k >= j ; ::_thesis: N . k in Q
A34: N . i <= N . k by A31, A32, A33;
 not N . i <= v1 by A28, A30, WAYBEL_0:17;
then  not N . k <= v1 by A34, ORDERS_2:3;
then  not N . k in downarrow v1 by WAYBEL_0:17;
hence  N . k in Q by A24, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
consider f being Function such that
A35: ( dom f = Z & rng f c= the carrier of N ) and
A36: for Q being set st Q in Z holds
S1[Q,f . Q] from FUNCT_1:sch_5(A22);
reconsider rngf = rng f as finite Subset of ([#] N) by A19, A35, FINSET_1:8;
 [#] N is directed by WAYBEL_0:def_6;
then consider k being Element of N such that
 k in [#] N and
A37: k is_>=_than rngf by WAYBEL_0:1;
take  k ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not k <= b1 or N . b1 in V )
let k1 be Element of N; ::_thesis: ( not k <= k1 or N . k1 in V )
assume A38: k <= k1 ; ::_thesis: N . k1 in V
now__::_thesis:_for_Q_being_set_st_Q_in_Z_holds_
N_._k1_in_Q
let Q be set ; ::_thesis: ( Q in Z implies N . k1 in Q )
assume A39: Q in Z ; ::_thesis: N . k1 in Q
then A40: f . Q in rngf by A35, FUNCT_1:def_3;
then reconsider j = f . Q as Element of N ;
 j <= k by A37, A40, LATTICE3:def_9;
hence  N . k1 in Q by A36, A38, A39, ORDERS_2:3; ::_thesis: verum
end;
then A41: N . k1 in Y1 by A20, SETFAM_1:43;
 Y1 c= union Y by A17, ZFMISC_1:74;
then A42: N . k1 in Int V by A15, A41;
 Int V c= V by TOPS_1:16;
hence  N . k1 in V by A42; ::_thesis: verum
end;
end;
hence  T is order_consistent by Def2; ::_thesis: verum
end;

theorem Th3: :: WAYBEL32:3
for R being non empty reflexive transitive antisymmetric up-complete RelStr ex T being TopAugmentation of R st T is Scott
proof
let R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: ex T being TopAugmentation of R st T is Scott
set T = the Scott TopAugmentation of R;
take  the Scott TopAugmentation of R ; ::_thesis: the Scott TopAugmentation of R is Scott
thus  the Scott TopAugmentation of R is Scott ; ::_thesis: verum
end;

theorem :: WAYBEL32:4
for R being non empty up-complete Poset
for T being TopAugmentation of R st T is Scott holds
T is correct ;

registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster Scott  ->  correct for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R st b1 is Scott holds
b1 is correct ;
end;

registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster non empty correct reflexive transitive antisymmetric up-complete Scott for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is Scott & b1 is correct )
proof
consider T being TopAugmentation of R such that
A1: T is Scott by Th3;
take  T ; ::_thesis: ( T is Scott & T is correct )
thus  ( T is Scott & T is correct ) by A1; ::_thesis: verum
end;
end;

theorem Th5: :: WAYBEL32:5
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds Cl {x} = downarrow x
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds Cl {x} = downarrow x
let x be Element of T; ::_thesis: Cl {x} = downarrow x
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
reconsider dx = downarrow x as Subset of T9 ;
reconsider A = {x} as Subset of T9 ;
A1: downarrow x is closed by WAYBEL11:11;
 x <= x ;
then  x in downarrow x by WAYBEL_0:17;
then A2: {x} c= downarrow x by ZFMISC_1:31;
now__::_thesis:_for_C_being_Subset_of_T9_st_A_c=_C_&_C_is_closed_holds_
dx_c=_C
let C be Subset of T9; ::_thesis: ( A c= C & C is closed implies dx c= C )
assume A3: A c= C ; ::_thesis: ( C is closed implies dx c= C )
reconsider D = C as Subset of T9 ;
assume  C is closed ; ::_thesis: dx c= C
then A4: D is lower by WAYBEL11:7;
 x in C by A3, ZFMISC_1:31;
hence  dx c= C by A4, WAYBEL11:6; ::_thesis: verum
end;
hence  Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum
end;

theorem Th6: :: WAYBEL32:6
for T being non empty up-complete Scott TopPoset holds T is order_consistent
proof
let T be non empty up-complete Scott TopPoset; ::_thesis: T is order_consistent
 for x being Element of T holds
( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
proof
let x be Element of T; ::_thesis: ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) )
 for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V
proof
let N be eventually-directed net of T; ::_thesis: ( x = sup N implies for V being a_neighborhood of x holds N is_eventually_in V )
assume  x = sup N ; ::_thesis: for V being a_neighborhood of x holds N is_eventually_in V
then  x = Sup by WAYBEL_2:def_1;
then A1: x = sup (rng the mapping of N) by YELLOW_2:def_5;
let V be a_neighborhood of x; ::_thesis: N is_eventually_in V
A2: x in Int V by CONNSP_2:def_1;
reconsider rngN = rng (netmap (N,T)) as Subset of T ;
 rngN is directed by WAYBEL_2:18;
then  Int V meets rngN by A1, A2, WAYBEL11:def_1;
then consider z being set  such that
A3: z in Int V and
A4: z in rngN by XBOOLE_0:3;
reconsider z9 = z as Element of T by A3;
consider i being set  such that
A5: i in dom the mapping of N and
A6: z9 = the mapping of N . i by A4, FUNCT_1:def_3;
reconsider i = i as Element of N by A5;
consider j being Element of N such that
A7: for k being Element of N st j <= k holds
N . i <= N . k by WAYBEL_0:11;
take  j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in V )
let l be Element of N; ::_thesis: ( not j <= l or N . l in V )
assume  j <= l ; ::_thesis: N . l in V
then  N . i <= N . l by A7;
then A8: N . l in Int V by A3, A6, WAYBEL_0:def_20;
 Int V c= V by TOPS_1:16;
hence  N . l in V by A8; ::_thesis: verum
end;
hence  ( downarrow x = Cl {x} & ( for N being eventually-directed net of T st x = sup N holds
for V being a_neighborhood of x holds N is_eventually_in V ) ) by Th5; ::_thesis: verum
end;
hence  T is order_consistent by Def2; ::_thesis: verum
end;

theorem Th7: :: WAYBEL32:7
for R being /\-complete Semilattice
for Z being net of R
for D being Subset of R st D =  {  ("/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R)) where j is Element of Z : verum  }  holds
( not D is empty & D is directed )
proof
let R be /\-complete Semilattice; ::_thesis: for Z being net of R
for D being Subset of R st D =  {  ("/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R)) where j is Element of Z : verum  }  holds
( not D is empty & D is directed )
let Z be net of R; ::_thesis: for D being Subset of R st D =  {  ("/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R)) where j is Element of Z : verum  }  holds
( not D is empty & D is directed )
let D be Subset of R; ::_thesis: ( D =  {  ("/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R)) where j is Element of Z : verum  }  implies ( not D is empty & D is directed ) )
assume A1: D =  {  ("/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R)) where j is Element of Z : verum  }  ; ::_thesis: ( not D is empty & D is directed )
set j = the Element of Z;
 "/\" ( {  (Z . k) where k is Element of Z : k >= the Element of Z  }  ,R) in D by A1;
hence  not D is empty ; ::_thesis: D is directed
let x, y be Element of R; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D or not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
assume  x in D ; ::_thesis: ( not y in D or ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 ) )
then consider jx being Element of Z such that
A2: x = "/\" ( {  (Z . k) where k is Element of Z : k >= jx  }  ,R) by A1;
assume  y in D ; ::_thesis: ex b1 being Element of the carrier of R st
( b1 in D & x <= b1 & y <= b1 )
then consider jy being Element of Z such that
A3: y = "/\" ( {  (Z . k) where k is Element of Z : k >= jy  }  ,R) by A1;
reconsider jx = jx, jy = jy as Element of Z ;
consider j being Element of Z such that
A4: j >= jx and
A5: j >= jy by YELLOW_6:def_3;
consider j9 being Element of Z such that
A6: j9 >= j and
 j9 >= j by YELLOW_6:def_3;
deffunc H1( Element of Z) ->  Element of the carrier of R = Z . $1;
defpred S1[ Element of Z] means $1 >= jx;
defpred S2[ Element of Z] means $1 >= jy;
defpred S3[ Element of Z] means $1 >= j;
set Ex =  {  H1(k) where k is Element of Z : S1[k]  }  ;
set Ey =  {  H1(k) where k is Element of Z : S2[k]  }  ;
set E =  {  H1(k) where k is Element of Z : S3[k]  }  ;
A7: Z . j in  {  H1(k) where k is Element of Z : S1[k]  }  by A4;
A8: Z . j in  {  H1(k) where k is Element of Z : S2[k]  }  by A5;
A9: Z . j9 in  {  H1(k) where k is Element of Z : S3[k]  }  by A6;
A10:  {  H1(k) where k is Element of Z : S1[k]  }  is Subset of R from DOMAIN_1:sch_8();
A11:  {  H1(k) where k is Element of Z : S2[k]  }  is Subset of R from DOMAIN_1:sch_8();
A12:  {  H1(k) where k is Element of Z : S3[k]  }  is Subset of R from DOMAIN_1:sch_8();
take z = "/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R); ::_thesis: ( z in D & x <= z & y <= z )
reconsider Ex9 =  {  H1(k) where k is Element of Z : S1[k]  }  as non empty Subset of R by A7, A10;
reconsider Ey9 =  {  H1(k) where k is Element of Z : S2[k]  }  as non empty Subset of R by A8, A11;
reconsider E9 =  {  H1(k) where k is Element of Z : S3[k]  }  as non empty Subset of R by A9, A12;
A13: ex_inf_of E9,R by WAYBEL_0:76;
A14: ex_inf_of Ex9,R by WAYBEL_0:76;
A15: ex_inf_of Ey9,R by WAYBEL_0:76;
thus  z in D by A1; ::_thesis: ( x <= z & y <= z )
 E9 c= Ex9
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ex9 )
assume  e in E9 ; ::_thesis: e in Ex9
then consider k being Element of Z such that
A16: e = Z . k and
A17: k >= j ;
reconsider k = k as Element of Z ;
 k >= jx by A4, A17, YELLOW_0:def_2;
hence  e in Ex9 by A16; ::_thesis: verum
end;
hence  x <= z by A2, A13, A14, YELLOW_0:35; ::_thesis: y <= z
 E9 c= Ey9
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in E9 or e in Ey9 )
assume  e in E9 ; ::_thesis: e in Ey9
then consider k being Element of Z such that
A18: e = Z . k and
A19: k >= j ;
reconsider k = k as Element of Z ;
 k >= jy by A5, A19, YELLOW_0:def_2;
hence  e in Ey9 by A18; ::_thesis: verum
end;
hence  y <= z by A3, A13, A15, YELLOW_0:35; ::_thesis: verum
end;

theorem Th8: :: WAYBEL32:8
for R being /\-complete Semilattice
for S being Subset of R
for a being Element of R st a in S holds
"/\" (S,R) <= a
proof
let R be /\-complete Semilattice; ::_thesis: for S being Subset of R
for a being Element of R st a in S holds
"/\" (S,R) <= a
let S be Subset of R; ::_thesis: for a being Element of R st a in S holds
"/\" (S,R) <= a
let a be Element of R; ::_thesis: ( a in S implies "/\" (S,R) <= a )
assume A1: a in S ; ::_thesis: "/\" (S,R) <= a
then  ex_inf_of S,R by WAYBEL_0:76;
then  S is_>=_than "/\" (S,R) by YELLOW_0:31;
hence  "/\" (S,R) <= a by A1, LATTICE3:def_8; ::_thesis: verum
end;

theorem Th9: :: WAYBEL32:9
for R being /\-complete Semilattice
for N being reflexive monotone net of R holds lim_inf N = sup N
proof
let R be /\-complete Semilattice; ::_thesis: for N being reflexive monotone net of R holds lim_inf N = sup N
let N be reflexive monotone net of R; ::_thesis: lim_inf N = sup N
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,R);
deffunc H2( Element of N) ->  Element of the carrier of R = N . $1;
defpred S1[ set ] means verum;
set X =  {  H1(j) where j is Element of N : S1[j]  }  ;
A1: for j being Element of N holds H2(j) = H1(j)
proof
let j be Element of N; ::_thesis: H2(j) = H1(j)
defpred S2[ Element of N] means $1 >= j;
set Y =  {  H2(i) where i is Element of N : S2[i]  }  ;
 j <= j ;
then A2: N . j in  {  H2(i) where i is Element of N : S2[i]  }  ;
  {  H2(i) where i is Element of N : S2[i]  }  is Subset of R from DOMAIN_1:sch_8();
then A3: ex_inf_of  {  H2(i) where i is Element of N : S2[i]  }  ,R by A2, WAYBEL_0:76;
A4: N . j is_<=_than  {  H2(i) where i is Element of N : S2[i]  }
proof
let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in  {  H2(i) where i is Element of N : S2[i]  }  or N . j <= y )
assume  y in  {  H2(i) where i is Element of N : S2[i]  }  ; ::_thesis: N . j <= y
then  ex i being Element of N st
( y = N . i & j <= i ) ;
hence  N . j <= y by WAYBEL11:def_9; ::_thesis: verum
end;
 for b being Element of R st b is_<=_than  {  H2(i) where i is Element of N : S2[i]  }  holds
N . j >= b
proof
let b be Element of R; ::_thesis: ( b is_<=_than  {  H2(i) where i is Element of N : S2[i]  }  implies N . j >= b )
assume A5: b is_<=_than  {  H2(i) where i is Element of N : S2[i]  }  ; ::_thesis: N . j >= b
reconsider j9 = j as Element of N ;
 j9 <= j9 ;
then  N . j9 in  {  H2(i) where i is Element of N : S2[i]  }  ;
hence  N . j >= b by A5, LATTICE3:def_8; ::_thesis: verum
end;
hence  H2(j) = H1(j) by A3, A4, YELLOW_0:def_10; ::_thesis: verum
end;
rng the mapping of N =  {  H2(j) where j is Element of N : S1[j]  }  by WAYBEL11:19
.=  {  H1(j) where j is Element of N : S1[j]  }  from FRAENKEL:sch_5(A1) ;
hence  lim_inf N = Sup by YELLOW_2:def_5
.= sup N by WAYBEL_2:def_1 ;
::_thesis: verum
end;

theorem Th10: :: WAYBEL32:10
for R being /\-complete Semilattice
for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
proof
let R be /\-complete Semilattice; ::_thesis: for S being Subset of R holds
( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence R;
set T = ConvergenceSpace (Scott-Convergence R);
A1: the topology of (ConvergenceSpace (Scott-Convergence R)) =  {  V where V is Subset of R : for p being Element of R st p in V holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in V  }  by YELLOW_6:def_24;
let S be Subset of R; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence R)) iff ( S is inaccessible & S is upper ) )
hereby  ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence R)) )
assume  S in the topology of (ConvergenceSpace (Scott-Convergence R)) ; ::_thesis: ( S is inaccessible & S is upper )
then A2: ex V being Subset of R st
( S = V & ( for p being Element of R st p in V holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in V ) ) by A1;
thus  S is inaccessible ::_thesis: S is upper
proof
let D be non empty directed Subset of R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in S or not D misses S )
assume A3: sup D in S ; ::_thesis: not D misses S
A4: dom (id D) = D by RELAT_1:45;
A5: rng (id D) = D by RELAT_1:45;
then reconsider f = id D as Function of D, the carrier of R by A4, FUNCT_2:def_1, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of R by A5, WAYBEL11:20;
A6: N in NetUniv R by WAYBEL11:21;
lim_inf N = sup N by Th9
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),R) by YELLOW_2:def_5
.= "\/" ((rng f),R) by WAYBEL11:def_10
.= sup D by RELAT_1:45 ;
then  sup D is_S-limit_of N by WAYBEL11:def_7;
then  [N,(sup D)] in Scott-Convergence R by A6, WAYBEL11:def_8;
then  N is_eventually_in S by A2, A3;
then consider i0 being Element of N such that
A7: for j being Element of N st i0 <= j holds
N . j in S by WAYBEL_0:def_11;
consider j0 being Element of N such that
A8: j0 >= i0 and
 j0 >= i0 by YELLOW_6:def_3;
A9: N . j0 in S by A7, A8;
A10: D = the carrier of N by WAYBEL11:def_10;
N . j0 = (id D) . j0 by WAYBEL11:def_10
.= j0 by A10, FUNCT_1:18 ;
hence  not D misses S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus  S is upper ::_thesis: verum
proof
let x, y be Element of R; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S )
assume that
A11: x in S and
A12: x <= y ; ::_thesis: y in S
A13: Net-Str y in NetUniv R by WAYBEL11:29;
 y = lim_inf (Net-Str y) by WAYBEL11:28;
then  x is_S-limit_of Net-Str y by A12, WAYBEL11:def_7;
then  [(Net-Str y),x] in Scott-Convergence R by A13, WAYBEL11:def_8;
then  Net-Str y is_eventually_in S by A2, A11;
hence  y in S by WAYBEL11:27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence R))
 for p being Element of R st p in S holds
for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
proof
let p be Element of R; ::_thesis: ( p in S implies for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of R st [N,p] in Scott-Convergence R holds
N is_eventually_in S
reconsider p9 = p as Element of R ;
let N be net of R; ::_thesis: ( [N,p] in Scott-Convergence R implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence R ; ::_thesis: N is_eventually_in S
 Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A18: N in NetUniv R by A17, ZFMISC_1:87;
then  ex N9 being strict net of R st
( N9 = N & the carrier of N9 in the_universe_of the carrier of R ) by YELLOW_6:def_11;
then  p is_S-limit_of N by A17, A18, WAYBEL11:def_8;
then A19: p9 <= lim_inf N by WAYBEL11:def_7;
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,R);
defpred S1[ set ] means verum;
set X =  {  H1(j) where j is Element of N : S1[j]  }  ;
  {  H1(j) where j is Element of N : S1[j]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
 sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then  D meets S by A14, WAYBEL11:def_1;
then  D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of R such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of R ;
 d in D by A20, XBOOLE_0:def_4;
then consider j being Element of N such that
A21: d = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R) ;
defpred S2[ Element of N] means $1 >= j;
deffunc H2( Element of N) ->  Element of the carrier of R = N . $1;
  {  H2(i) where i is Element of N : S2[i]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider Y =  {  (N . i) where i is Element of N : i >= j  }  as Subset of R ;
reconsider j = j as Element of N ;
take  j ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j <= b1 or N . b1 in S )
let i0 be Element of N; ::_thesis: ( not j <= i0 or N . i0 in S )
A22: d in S by A20, XBOOLE_0:def_4;
assume  j <= i0 ; ::_thesis: N . i0 in S
then  N . i0 in Y ;
then  d <= N . i0 by A21, Th8;
hence  N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
hence  S in the topology of (ConvergenceSpace (Scott-Convergence R)) by A1; ::_thesis: verum
end;

theorem Th11: :: WAYBEL32:11
for R being up-complete /\-complete Semilattice
for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
proof
let R be up-complete /\-complete Semilattice; ::_thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
let T be TopAugmentation of R; ::_thesis: ( the topology of T = sigma R implies T is Scott )
assume A1: the topology of T = sigma R ; ::_thesis: T is Scott
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
 T is Scott
proof
let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( ( not S is open or ( S is inaccessible_by_directed_joins & S is upper ) ) & ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) )
reconsider A = S as Subset of R by A2;
thus  ( S is open implies ( S is inaccessible & S is upper ) ) ::_thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open )
proof
assume  S is open ; ::_thesis: ( S is inaccessible & S is upper )
then  S in the topology of T by PRE_TOPC:def_2;
then  ( A is inaccessible & A is upper ) by A1, Th10;
hence  ( S is inaccessible & S is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; ::_thesis: verum
end;
assume A3: ( S is inaccessible & S is upper ) ; ::_thesis: S is open
 A is inaccessible
proof
let D be non empty directed Subset of R; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,R) in A or not D misses A )
assume A4: sup D in A ; ::_thesis: not D misses A
reconsider E = D as Subset of T by A2;
 ex a being Element of R st
( a is_>=_than D & ( for b being Element of R st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A5: ex_sup_of D,R by YELLOW_0:15;
A6: E is directed by A2, WAYBEL_0:3;
 sup D = sup E by A2, A5, YELLOW_0:26;
hence  not D misses A by A3, A4, A6, WAYBEL11:def_1; ::_thesis: verum
end;
then  ( A is inaccessible & A is upper ) by A2, A3, WAYBEL_0:25;
then  A in the topology of T by A1, Th10;
hence  S is open by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  T is Scott ; ::_thesis: verum
end;

registration
let R be up-complete /\-complete Semilattice;
cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for TopAugmentation of R;
existence
 ex b1 being TopAugmentation of R st
( b1 is strict & b1 is Scott & b1 is correct )
proof
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
 RelStr(# the carrier of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #), the InternalRel of TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) #) = RelStr(# the carrier of R, the InternalRel of R #) ;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopAugmentation of R by YELLOW_9:def_4;
take  T ; ::_thesis: ( T is strict & T is Scott & T is correct )
thus  ( T is strict & T is Scott & T is correct ) by Th11, YELLOW_9:48; ::_thesis: verum
end;
end;

theorem :: WAYBEL32:12
for S being up-complete /\-complete Semilattice
for T being Scott TopAugmentation of S holds sigma S = the topology of T
proof
let S be up-complete /\-complete Semilattice; ::_thesis: for T being Scott TopAugmentation of S holds sigma S = the topology of T
let T be Scott TopAugmentation of S; ::_thesis: sigma S = the topology of T
thus  sigma S c= the topology of T :: according to XBOOLE_0:def_10 ::_thesis: the topology of T c= sigma S
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in sigma S or e in the topology of T )
assume A1: e in sigma S ; ::_thesis: e in the topology of T
then reconsider A = e as Subset of S ;
A2: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of T ;
 ( A is inaccessible & A is upper ) by A1, Th10;
then  ( A9 is inaccessible & A9 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
hence  e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in sigma S )
assume A3: e in the topology of T ; ::_thesis: e in sigma S
then reconsider A = e as Subset of T ;
A4: A is open by A3, PRE_TOPC:def_2;
A5: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def_4;
then reconsider A9 = A as Subset of S ;
 A9 is inaccessible
proof
let D be non empty directed Subset of S; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,S) in A9 or not D misses A9 )
assume A6: sup D in A9 ; ::_thesis: not D misses A9
reconsider E = D as Subset of T by A5;
 ex a being Element of S st
( a is_>=_than D & ( for b being Element of S st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A7: ex_sup_of D,S by YELLOW_0:15;
A8: E is directed by A5, WAYBEL_0:3;
 sup D = sup E by A5, A7, YELLOW_0:26;
hence  not D misses A9 by A4, A6, A8, WAYBEL11:def_1; ::_thesis: verum
end;
then  ( A9 is inaccessible & A9 is upper ) by A4, A5, WAYBEL_0:25;
hence  e in sigma S by Th10; ::_thesis: verum
end;

theorem :: WAYBEL32:13
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr holds T is T_0-TopSpace
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: T is T_0-TopSpace
reconsider T9 = T as Scott TopAugmentation of T by YELLOW_9:44;
now__::_thesis:_for_x,_y_being_Point_of_T9_st_x_<>_y_holds_
Cl_{x}_<>_Cl_{y}
let x, y be Point of T9; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
reconsider x9 = x, y9 = y as Element of T9 ;
A1: Cl {x9} = downarrow x9 by Th5;
A2: Cl {y9} = downarrow y9 by Th5;
assume  x <> y ; ::_thesis: Cl {x} <> Cl {y}
hence  Cl {x} <> Cl {y} by A1, A2, WAYBEL_0:19; ::_thesis: verum
end;
hence  T is T_0-TopSpace by TSP_1:def_5; ::_thesis: verum
end;

registration
let R be non empty reflexive transitive antisymmetric up-complete RelStr ;
cluster  ->  up-complete for TopAugmentation of R;
coherence
 for b1 being TopAugmentation of R holds b1 is up-complete ;
end;

theorem Th14: :: WAYBEL32:14
for R being non empty reflexive transitive antisymmetric up-complete RelStr
for T being Scott TopAugmentation of R
for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
proof
let R be non empty reflexive transitive antisymmetric up-complete RelStr ; ::_thesis: for T being Scott TopAugmentation of R
for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let T be Scott TopAugmentation of R; ::_thesis: for x being Element of T
for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds
(downarrow x) ` is a_neighborhood of A
let A be upper Subset of T; ::_thesis: ( not x in A implies (downarrow x) ` is a_neighborhood of A )
assume A1: not x in A ; ::_thesis: (downarrow x) ` is a_neighborhood of A
 downarrow x is closed by WAYBEL11:11;
then  (downarrow x) ` is open ;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
 A misses downarrow x by A1, WAYBEL11:5;
then  A c= (downarrow x) ` by SUBSET_1:23;
hence  (downarrow x) ` is a_neighborhood of A by A2, CONNSP_2:def_2; ::_thesis: verum
end;

theorem :: WAYBEL32:15
for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for T being Scott TopAugmentation of R
for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
proof
let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for T being Scott TopAugmentation of R
for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
let T be Scott TopAugmentation of R; ::_thesis: for S being upper Subset of T ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
let S be upper Subset of T; ::_thesis: ex F being Subset-Family of T st
( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
defpred S1[ set ] means $1 is a_neighborhood of S;
set F =  {  X where X is Subset of T : S1[X]  }  ;
  {  X where X is Subset of T : S1[X]  }  is Subset-Family of T from DOMAIN_1:sch_7();
then reconsider F =  {  X where X is Subset of T : S1[X]  }  as Subset-Family of T ;
take  F ; ::_thesis: ( S = meet F & ( for X being Subset of T st X in F holds
X is a_neighborhood of S ) )
thus  S = meet F ::_thesis: for X being Subset of T st X in F holds
X is a_neighborhood of S
proof
 [#] T is a_neighborhood of S by CONNSP_2:28;
then A1: [#] T in F ;
now__::_thesis:_for_Z1_being_set_st_Z1_in_F_holds_
S_c=_Z1
let Z1 be set ; ::_thesis: ( Z1 in F implies S c= Z1 )
assume  Z1 in F ; ::_thesis: S c= Z1
then  ex X being Subset of T st
( Z1 = X & X is a_neighborhood of S ) ;
hence  S c= Z1 by CONNSP_2:29; ::_thesis: verum
end;
hence  S c= meet F by A1, SETFAM_1:5; :: according to XBOOLE_0:def_10 ::_thesis: meet F c= S
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet F or x in S )
assume that
A2: x in meet F and
A3: not x in S ; ::_thesis: contradiction
reconsider p = x as Element of T by A2;
 (downarrow p) ` is a_neighborhood of S by A3, Th14;
then  (downarrow p) ` in F ;
then A4: meet F c= (downarrow p) ` by SETFAM_1:3;
 p <= p ;
then  p in downarrow p by WAYBEL_0:17;
hence  contradiction by A2, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
let X be Subset of T; ::_thesis: ( X in F implies X is a_neighborhood of S )
assume  X in F ; ::_thesis: X is a_neighborhood of S
then  ex Y being Subset of T st
( X = Y & Y is a_neighborhood of S ) ;
hence  X is a_neighborhood of S ; ::_thesis: verum
end;

theorem :: WAYBEL32:16
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
let S be Subset of T; ::_thesis: ( S is open iff ( S is upper & S is property(S) ) )
hereby  ::_thesis: ( S is upper & S is property(S) implies S is open )
assume A1: S is open ; ::_thesis: ( S is upper & S is property(S) )
hence  S is upper ; ::_thesis: S is property(S)
thus  S is property(S) ::_thesis: verum
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) ) )
assume  sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) )
then  S meets D by A1, WAYBEL11:def_1;
then consider y being set  such that
A2: y in S and
A3: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
take  y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) )
thus  ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) ) by A1, A2, A3, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
assume that
A4: S is upper and
A5: S is property(S) ; ::_thesis: S is open
 S is inaccessible
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,T) in S or not D misses S )
assume  sup D in S ; ::_thesis: not D misses S
then consider y being Element of T such that
A6: y in D and
A7: for x being Element of T st x in D & x >= y holds
x in S by A5, WAYBEL11:def_3;
 y >= y by YELLOW_0:def_1;
then  y in S by A6, A7;
hence  not D misses S by A6, XBOOLE_0:3; ::_thesis: verum
end;
hence  S is open by A4; ::_thesis: verum
end;

theorem Th17: :: WAYBEL32:17
for R being non empty reflexive transitive antisymmetric up-complete TopRelStr
for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)
proof
let R be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for S being non empty directed Subset of R
for a being Element of R st a in S holds
a <= "\/" (S,R)
let S be non empty directed Subset of R; ::_thesis: for a being Element of R st a in S holds
a <= "\/" (S,R)
let a be Element of R; ::_thesis: ( a in S implies a <= "\/" (S,R) )
assume A1: a in S ; ::_thesis: a <= "\/" (S,R)
 ex_sup_of S,R by WAYBEL_0:75;
then  S is_<=_than "\/" (S,R) by YELLOW_0:30;
hence  a <= "\/" (S,R) by A1, LATTICE3:def_9; ::_thesis: verum
end;

registration
let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ;
cluster lower  ->  property(S) for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is lower holds
b1 is property(S)
proof
let S be Subset of T; ::_thesis: ( S is lower implies S is property(S) )
assume A1: S is lower ; ::_thesis: S is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( not "\/" (D,T) in S or ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) ) )
assume A2: sup D in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in D & ( for b2 being Element of the carrier of T holds
( not b2 in D or not b1 <= b2 or b2 in S ) ) )
consider y being Element of T such that
A3: y in D by SUBSET_1:4;
take  y ; ::_thesis: ( y in D & ( for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S ) ) )
thus  y in D by A3; ::_thesis: for b1 being Element of the carrier of T holds
( not b1 in D or not y <= b1 or b1 in S )
let x be Element of T; ::_thesis: ( not x in D or not y <= x or x in S )
assume that
A4: x in D and
 x >= y ; ::_thesis: x in S
 x <= sup D by A4, Th17;
hence  x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
end;

theorem :: WAYBEL32:18
for T being non empty finite up-complete Poset
for S being Subset of T holds S is inaccessible
proof
let T be non empty finite up-complete Poset; ::_thesis: for S being Subset of T holds S is inaccessible
let S be Subset of T; ::_thesis: S is inaccessible
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( not "\/" (D,T) in S or not D misses S )
assume A1: sup D in S ; ::_thesis: not D misses S
 sup D in D
proof
reconsider D9 = D as finite Subset of T ;
 D9 c= D9 ;
then reconsider E = D9 as finite Subset of D ;
consider x being Element of T such that
A2: x in D and
A3: x is_>=_than E by WAYBEL_0:1;
A4: for b being Element of T st D is_<=_than b holds
b >= x by A2, LATTICE3:def_9;
 for c being Element of T st D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) holds
c = x
proof
let c be Element of T; ::_thesis: ( D is_<=_than c & ( for b being Element of T st D is_<=_than b holds
b >= c ) implies c = x )
assume that
A5: D is_<=_than c and
A6: for b being Element of T st D is_<=_than b holds
b >= c ; ::_thesis: c = x
A7: x >= c by A3, A6;
 c >= x by A2, A5, LATTICE3:def_9;
hence  c = x by A7, ORDERS_2:2; ::_thesis: verum
end;
then  ex_sup_of D,T by A3, A4, YELLOW_0:def_7;
hence  sup D in D by A2, A3, A4, YELLOW_0:def_9; ::_thesis: verum
end;
hence  not D misses S by A1, XBOOLE_0:3; ::_thesis: verum
end;

theorem Th19: :: WAYBEL32:19
for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
proof
let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R
for x being Element of T holds (downarrow x) ` is open
let T be Scott TopAugmentation of R; ::_thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; ::_thesis: (downarrow x) ` is open
reconsider S = downarrow x as lower directly_closed Subset of T by WAYBEL11:8;
 S ` is open ;
hence  (downarrow x) ` is open ; ::_thesis: verum
end;

theorem :: WAYBEL32:20
for R being complete connected LATTICE
for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) )
proof
let R be complete connected LATTICE; ::_thesis: for T being Scott TopAugmentation of R
for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) )
let T be Scott TopAugmentation of R; ::_thesis: for S being Subset of T holds
( S is open iff ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) )
let S be Subset of T; ::_thesis: ( S is open iff ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) )
set DD =  {  ((downarrow x) `) where x is Element of T : verum  }  ;
thus  ( not S is open or S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) ::_thesis: ( ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) implies S is open )
proof
assume A1: S is open ; ::_thesis: ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  )
assume that
A2: S <> the carrier of T and
A3: not S in  {  ((downarrow x) `) where x is Element of T : verum  }  ; ::_thesis: contradiction
A4: ([#] T) \ S <> {} by A2, PRE_TOPC:4;
A5: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then reconsider K = S ` as Subset of R ;
reconsider D = K as non empty directed Subset of T by A4, A5, WAYBEL_0:3;
A6: D misses S by SUBSET_1:23;
reconsider x = sup D as Element of T ;
 S ` = downarrow x
proof
thus  S ` c= downarrow x :: according to XBOOLE_0:def_10 ::_thesis: downarrow x c= S `
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in S ` or a in downarrow x )
assume A7: a in S ` ; ::_thesis: a in downarrow x
then reconsider A = a as Element of T ;
 x is_>=_than S ` by YELLOW_0:32;
then  A <= x by A7, LATTICE3:def_9;
hence  a in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in downarrow x or a in S ` )
assume A8: a in downarrow x ; ::_thesis: a in S `
then reconsider A = a as Element of T ;
A9: A <= x by A8, WAYBEL_0:17;
 not x in S by A1, A6, WAYBEL11:def_1;
then  not A in S by A1, A9, WAYBEL_0:def_20;
hence  a in S ` by XBOOLE_0:def_5; ::_thesis: verum
end;
then  (downarrow x) ` = S ;
hence  contradiction by A3; ::_thesis: verum
end;
assume A10: ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) ; ::_thesis: S is open
percases ( S = the carrier of T or S in  {  ((downarrow x) `) where x is Element of T : verum  }  ) by A10;
supposeA11: S = the carrier of T ; ::_thesis: S is open
A12: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def_4;
then  S = [#] R by A11;
then A13: S is inaccessible by A12, YELLOW_9:47;
 S is upper
proof
let x, y be Element of T; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in S or not x <= y or y in S )
assume that
 x in S and
 x <= y ; ::_thesis: y in S
thus  y in S by A11; ::_thesis: verum
end;
hence  S is open by A13; ::_thesis: verum
end;
suppose S in  {  ((downarrow x) `) where x is Element of T : verum  }  ; ::_thesis: S is open
then  ex x being Element of T st S = (downarrow x) ` ;
hence  S is open by Th19; ::_thesis: verum
end;
end;
end;

registration
let R be non empty up-complete Poset;
cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for TopAugmentation of R;
correctness
existence
ex b1 being correct TopAugmentation of R st b1 is order_consistent ;
proof
set T = the correct Scott TopAugmentation of R;
take  the correct Scott TopAugmentation of R ; ::_thesis: the correct Scott TopAugmentation of R is order_consistent
thus  the correct Scott TopAugmentation of R is order_consistent by Th6; ::_thesis: verum
end;
end;

registration
cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete order_consistent for TopRelStr ;
correctness
existence
ex b1 being TopLattice st
( b1 is order_consistent & b1 is complete );
proof
set T = the complete Scott TopLattice;
take  the complete Scott TopLattice ; ::_thesis: ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete )
thus  ( the complete Scott TopLattice is order_consistent & the complete Scott TopLattice is complete ) by Th6; ::_thesis: verum
end;
end;

theorem Th21: :: WAYBEL32:21
for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper
proof
let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper
let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) & A is open implies A is upper )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: ( not A is open or A is upper )
assume A2: A is open ; ::_thesis: A is upper
let x, y be Element of R; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in A or not x <= y or y in A )
assume that
A3: x in A and
A4: x <= y ; ::_thesis: y in A
 x in downarrow y by A4, WAYBEL_0:17;
then  x in Cl {y} by A1;
then  A meets {y} by A2, A3, PRE_TOPC:24;
then consider z being set  such that
A5: z in A /\ {y} by XBOOLE_0:4;
A6: z in A by A5, XBOOLE_0:def_4;
 z in {y} by A5, XBOOLE_0:def_4;
hence  y in A by A6, TARSKI:def_1; ::_thesis: verum
end;

theorem :: WAYBEL32:22
for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower
proof
let R be non empty TopRelStr ; ::_thesis: for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) holds
for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; ::_thesis: ( ( for x being Element of R holds downarrow x = Cl {x} ) implies for A being Subset of R st A is closed holds
A is lower )
assume A1: for x being Element of R holds downarrow x = Cl {x} ; ::_thesis: for A being Subset of R st A is closed holds
A is lower
let A be Subset of R; ::_thesis: ( A is closed implies A is lower )
assume A2: A is closed ; ::_thesis: A is lower
let x, y be Element of R; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in A or not y <= x or y in A )
assume that
A3: x in A and
A4: y <= x ; ::_thesis: y in A
 y in downarrow x by A4, WAYBEL_0:17;
then A5: y in Cl {x} by A1;
 {x} c= A
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in A )
assume  a in {x} ; ::_thesis: a in A
hence  a in A by A3, TARSKI:def_1; ::_thesis: verum
end;
hence  y in A by A2, A5, PRE_TOPC:15; ::_thesis: verum
end;

definition
let S be non empty 1-sorted ;
let R be non empty RelStr ;
let f be Function of the carrier of R, the carrier of S;
funcR *' f ->  non empty strict NetStr over S means :Def3: :: WAYBEL32:def 3
( RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of it = f );
existence
 ex b1 being non empty strict NetStr over S st
( RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f )
proof
reconsider M = NetStr(# the carrier of R, the InternalRel of R,f #) as non empty strict NetStr over S ;
take  M ; ::_thesis: ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f )
thus  ( RelStr(# the carrier of M, the InternalRel of M #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of M = f ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict NetStr over S st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b1 = f & RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b2 = f holds
b1 = b2 ;
end;

:: deftheorem Def3 defines *' WAYBEL32:def_3_:_
 for S being non empty 1-sorted
for R being non empty RelStr
for f being Function of the carrier of R, the carrier of S
for b4 being non empty strict NetStr over S holds
( b4 = R *' f iff ( RelStr(# the carrier of b4, the InternalRel of b4 #) = RelStr(# the carrier of R, the InternalRel of R #) & the mapping of b4 = f ) );

registration
let S be non empty 1-sorted ;
let R be non empty transitive RelStr ;
let f be Function of the carrier of R, the carrier of S;
clusterR *' f ->  non empty transitive strict ;
coherence
 R *' f is transitive
proof
 RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3;
hence  R *' f is transitive by WAYBEL_8:13; ::_thesis: verum
end;
end;

registration
let S be non empty 1-sorted ;
let R be non empty directed RelStr ;
let f be Function of the carrier of R, the carrier of S;
clusterR *' f ->  non empty strict directed ;
coherence
 R *' f is directed
proof
A1: RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by Def3;
 [#] R is directed by WAYBEL_0:def_6;
hence  [#] (R *' f) is directed by A1, WAYBEL_0:3; :: according to WAYBEL_0:def_6 ::_thesis: verum
end;
end;

definition
let R be non empty RelStr ;
let N be prenet of R;
func inf_net N ->  strict prenet of R means :Def4: :: WAYBEL32:def 4
 ex f being Function of N,R st
( it = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) );
existence
 ex b1 being strict prenet of R ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) )
proof
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . k) where k is Element of N : k >= $1  }  ,R);
consider g being Function of the carrier of N, the carrier of R such that
A1: for i being Element of N holds g . i = H1(i) from FUNCT_2:sch_4();
reconsider f = g as Function of N,R ;
reconsider M = N *' f as strict prenet of R ;
take  M ; ::_thesis: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) )
thus  ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict prenet of R st ex f being Function of N,R st
( b1 = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) & ex f being Function of N,R st
( b2 = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) holds
b1 = b2
proof
let M, P be strict prenet of R; ::_thesis: ( ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) & ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) implies M = P )
assume that
A2: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) and
A3: ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) ; ::_thesis: M = P
consider f1 being Function of N,R such that
A4: M = N *' f1 and
A5: for i being Element of N holds f1 . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by A2;
consider f2 being Function of N,R such that
A6: P = N *' f2 and
A7: for i being Element of N holds f2 . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by A3;
 for i being set st i in the carrier of N holds
f1 . i = f2 . i
proof
let i be set ; ::_thesis: ( i in the carrier of N implies f1 . i = f2 . i )
assume  i in the carrier of N ; ::_thesis: f1 . i = f2 . i
then reconsider i = i as Element of N ;
f1 . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by A5
.= f2 . i by A7 ;
hence  f1 . i = f2 . i ; ::_thesis: verum
end;
hence  M = P by A4, A6, FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines inf_net WAYBEL32:def_4_:_
 for R being non empty RelStr
for N being prenet of R
for b3 being strict prenet of R holds
( b3 = inf_net N iff ex f being Function of N,R st
( b3 = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) );

registration
let R be non empty RelStr ;
let N be net of R;
cluster inf_net N ->  transitive strict ;
coherence
 inf_net N is transitive
proof
 ex f being Function of N,R st
( inf_net N = N *' f & ( for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) ) ) by Def4;
hence  inf_net N is transitive ; ::_thesis: verum
end;
end;

registration
let R be non empty RelStr ;
let N be net of R;
cluster inf_net N ->  strict ;
coherence
 inf_net N is directed ;
end;

registration
let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N ->  strict monotone ;
coherence
 inf_net N is monotone
proof
let i, j be Element of (inf_net N); :: according to WAYBEL11:def_9 ::_thesis: ( not i <= j or (inf_net N) . i <= (inf_net N) . j )
assume A1: i <= j ; ::_thesis: (inf_net N) . i <= (inf_net N) . j
consider f being Function of N,R such that
A2: inf_net N = N *' f and
A3: for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by Def4;
A4: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A2, Def3;
then reconsider i9 = i, j9 = j as Element of N ;
deffunc H1( Element of N) ->  Element of the carrier of R = N . R;
defpred S1[ Element of N] means R >= j9;
defpred S2[ Element of N] means R >= i9;
set J =  {  H1(k) where k is Element of N : S1[k]  }  ;
set I =  {  H1(k) where k is Element of N : S2[k]  }  ;
A5:  {  H1(k) where k is Element of N : S1[k]  }  is Subset of R from DOMAIN_1:sch_8();
consider j0 being Element of N such that
A6: j0 >= j9 and
 j0 >= j9 by YELLOW_6:def_3;
 N . j0 in  {  H1(k) where k is Element of N : S1[k]  }  by A6;
then reconsider J9 =  {  H1(k) where k is Element of N : S1[k]  }  as non empty Subset of R by A5;
A7:  {  H1(k) where k is Element of N : S2[k]  }  is Subset of R from DOMAIN_1:sch_8();
consider j1 being Element of N such that
A8: j1 >= i9 and
 j1 >= i9 by YELLOW_6:def_3;
 N . j1 in  {  H1(k) where k is Element of N : S2[k]  }  by A8;
then reconsider I9 =  {  H1(k) where k is Element of N : S2[k]  }  as non empty Subset of R by A7;
A9: ex_inf_of J9,R by WAYBEL_0:76;
A10: ex_inf_of I9,R by WAYBEL_0:76;
A11: J9 c= I9
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in J9 or a in I9 )
assume A12: a in J9 ; ::_thesis: a in I9
then reconsider x = a as Element of R ;
consider k being Element of N such that
A13: x = N . k and
A14: k >= j9 by A12;
reconsider k9 = k as Element of N ;
 i9 <= j9 by A1, A4, YELLOW_0:1;
then  i9 <= k9 by A14, YELLOW_0:def_2;
hence  a in I9 by A13; ::_thesis: verum
end;
A15: f . i9 = "/\" ( {  H1(k) where k is Element of N : S2[k]  }  ,R) by A3;
A16: f . j9 = "/\" ( {  H1(k) where k is Element of N : S1[k]  }  ,R) by A3;
 the mapping of (inf_net N) = f by A2, Def3;
hence  (inf_net N) . i <= (inf_net N) . j by A9, A10, A11, A15, A16, YELLOW_0:35; ::_thesis: verum
end;
end;

registration
let R be non empty reflexive antisymmetric /\-complete RelStr ;
let N be net of R;
cluster inf_net N ->  strict eventually-directed ;
coherence
 inf_net N is eventually-directed ;
end;

theorem Th23: :: WAYBEL32:23
for R being non empty RelStr
for N being net of R holds rng the mapping of (inf_net N) =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
proof
let R be non empty RelStr ; ::_thesis: for N being net of R holds rng the mapping of (inf_net N) =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
let N be net of R; ::_thesis: rng the mapping of (inf_net N) =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
A4: the mapping of (inf_net N) = f by A1, Def3;
then A5: the carrier of (inf_net N) = dom f by FUNCT_2:def_1;
thus  rng the mapping of (inf_net N) c=  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  c= rng the mapping of (inf_net N)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of (inf_net N) or e in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  )
assume  e in rng the mapping of (inf_net N) ; ::_thesis: e in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
then consider u being set  such that
A6: u in dom f and
A7: e = f . u by A4, FUNCT_1:def_3;
reconsider u = u as Element of N by A6;
 f . u = "/\" ( {  (N . k) where k is Element of N : k >= u  }  ,R) by A2;
hence  e in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  by A7; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  or e in rng the mapping of (inf_net N) )
assume  e in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ; ::_thesis: e in rng the mapping of (inf_net N)
then consider j being Element of N such that
A8: e = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R) ;
 e = the mapping of (inf_net N) . j by A2, A4, A8;
hence  e in rng the mapping of (inf_net N) by A3, A4, A5, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th24: :: WAYBEL32:24
for R being up-complete /\-complete LATTICE
for N being net of R holds sup (inf_net N) = lim_inf N
proof
let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R holds sup (inf_net N) = lim_inf N
let N be net of R; ::_thesis: sup (inf_net N) = lim_inf N
defpred S1[ set ] means verum;
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . l) where l is Element of N : l >= $1  }  ,R);
sup (inf_net N) = Sup by WAYBEL_2:def_1
.= sup (rng the mapping of (inf_net N)) by YELLOW_2:def_5
.= lim_inf N by Th23 ;
hence  sup (inf_net N) = lim_inf N ; ::_thesis: verum
end;

theorem :: WAYBEL32:25
for R being up-complete /\-complete LATTICE
for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
proof
let R be up-complete /\-complete LATTICE; ::_thesis: for N being net of R
for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let N be net of R; ::_thesis: for i being Element of N holds sup (inf_net N) = lim_inf (N | i)
let i be Element of N; ::_thesis: sup (inf_net N) = lim_inf (N | i)
 sup (inf_net N) = lim_inf N by Th24;
hence  sup (inf_net N) = lim_inf (N | i) by WAYBEL21:41; ::_thesis: verum
end;

theorem Th26: :: WAYBEL32:26
for R being /\-complete Semilattice
for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
proof
let R be /\-complete Semilattice; ::_thesis: for N being net of R
for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let N be net of R; ::_thesis: for V being upper Subset of R st inf_net N is_eventually_in V holds
N is_eventually_in V
let V be upper Subset of R; ::_thesis: ( inf_net N is_eventually_in V implies N is_eventually_in V )
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
assume  inf_net N is_eventually_in V ; ::_thesis: N is_eventually_in V
then consider i being Element of (inf_net N) such that
A4: for j being Element of (inf_net N) st i <= j holds
(inf_net N) . j in V by WAYBEL_0:def_11;
consider j0 being Element of (inf_net N) such that
A5: i <= j0 and
 i <= j0 by YELLOW_6:def_3;
A6: (inf_net N) . j0 in V by A4, A5;
reconsider j9 = j0 as Element of N by A3;
take  j9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds
( not j9 <= b1 or N . b1 in V )
let j be Element of N; ::_thesis: ( not j9 <= j or N . j in V )
assume A7: j9 <= j ; ::_thesis: N . j in V
defpred S1[ Element of N] means $1 >= j9;
deffunc H1( Element of N) ->  Element of the carrier of R = N . $1;
set E =  {  H1(k) where k is Element of N : S1[k]  }  ;
  {  H1(k) where k is Element of N : S1[k]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider E =  {  H1(k) where k is Element of N : S1[k]  }  as Subset of R ;
 the mapping of (inf_net N) = f by A1, Def3;
then A8: (inf_net N) . j0 = "/\" (E,R) by A2;
 N . j in E by A7;
then  "/\" (E,R) <= N . j by Th8;
hence  N . j in V by A6, A8, WAYBEL_0:def_20; ::_thesis: verum
end;

theorem :: WAYBEL32:27
for R being /\-complete Semilattice
for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
proof
let R be /\-complete Semilattice; ::_thesis: for N being net of R
for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let N be net of R; ::_thesis: for V being lower Subset of R st N is_eventually_in V holds
inf_net N is_eventually_in V
let V be lower Subset of R; ::_thesis: ( N is_eventually_in V implies inf_net N is_eventually_in V )
consider f being Function of N,R such that
A1: inf_net N = N *' f and
A2: for i being Element of N holds f . i = "/\" ( {  (N . k) where k is Element of N : k >= i  }  ,R) by Def4;
A3: RelStr(# the carrier of (inf_net N), the InternalRel of (inf_net N) #) = RelStr(# the carrier of N, the InternalRel of N #) by A1, Def3;
assume  N is_eventually_in V ; ::_thesis: inf_net N is_eventually_in V
then consider i being Element of N such that
A4: for j being Element of N st i <= j holds
N . j in V by WAYBEL_0:def_11;
reconsider i9 = i as Element of (inf_net N) by A3;
take  i9 ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (inf_net N) holds
( not i9 <= b1 or (inf_net N) . b1 in V )
let j be Element of (inf_net N); ::_thesis: ( not i9 <= j or (inf_net N) . j in V )
assume A5: i9 <= j ; ::_thesis: (inf_net N) . j in V
reconsider j0 = j as Element of N by A3;
defpred S1[ Element of N] means $1 >= j0;
deffunc H1( Element of N) ->  Element of the carrier of R = N . $1;
set E =  {  H1(k) where k is Element of N : S1[k]  }  ;
consider j1 being Element of N such that
A6: j1 >= j0 and
 j1 >= j0 by YELLOW_6:def_3;
  {  H1(k) where k is Element of N : S1[k]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider E =  {  H1(k) where k is Element of N : S1[k]  }  as Subset of R ;
 i <= j0 by A3, A5, YELLOW_0:1;
then  i <= j1 by A6, YELLOW_0:def_2;
then A7: N . j1 in V by A4;
 N . j1 in E by A6;
then A8: "/\" (E,R) <= N . j1 by Th8;
 the mapping of (inf_net N) = f by A1, Def3;
then  (inf_net N) . j = "/\" (E,R) by A2;
hence  (inf_net N) . j in V by A7, A8, WAYBEL_0:def_19; ::_thesis: verum
end;

theorem Th28: :: WAYBEL32:28
for R being non empty up-complete /\-complete order_consistent TopLattice
for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
proof
let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being net of R
for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let N be net of R; ::_thesis: for x being Element of R st x <= lim_inf N holds
x is_a_cluster_point_of N
let x be Element of R; ::_thesis: ( x <= lim_inf N implies x is_a_cluster_point_of N )
assume A1: x <= lim_inf N ; ::_thesis: x is_a_cluster_point_of N
defpred S1[ Element of N] means verum;
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,R);
set X =  {  H1(j) where j is Element of N : S1[j]  }  ;
  {  H1(j) where j is Element of N : S1[j]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
 sup D = lim_inf N ;
then A2: sup D = sup (inf_net N) by Th24;
let V be a_neighborhood of x; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in V
 for a being Element of R holds downarrow a = Cl {a} by Def2;
then A3: Int V is upper by Th21;
 x in Int V by CONNSP_2:def_1;
then  sup D in Int V by A1, A3, WAYBEL_0:def_20;
then reconsider W = Int V as a_neighborhood of sup D by CONNSP_2:3;
A4: Int V c= V by TOPS_1:16;
 inf_net N is_eventually_in W by A2, Def2;
then  N is_eventually_in W by A3, Th26;
then  N is_eventually_in V by A4, WAYBEL_0:8;
hence  N is_often_in V by YELLOW_6:19; ::_thesis: verum
end;

theorem :: WAYBEL32:29
for R being non empty up-complete /\-complete order_consistent TopLattice
for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
proof
let R be non empty up-complete /\-complete order_consistent TopLattice; ::_thesis: for N being eventually-directed net of R
for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let N be eventually-directed net of R; ::_thesis: for x being Element of R holds
( x <= lim_inf N iff x is_a_cluster_point_of N )
let x be Element of R; ::_thesis: ( x <= lim_inf N iff x is_a_cluster_point_of N )
thus  ( x <= lim_inf N implies x is_a_cluster_point_of N ) by Th28; ::_thesis: ( x is_a_cluster_point_of N implies x <= lim_inf N )
thus  ( x is_a_cluster_point_of N implies x <= lim_inf N ) ::_thesis: verum
proof
assume A1: x is_a_cluster_point_of N ; ::_thesis: x <= lim_inf N
defpred S1[ Element of N] means verum;
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,R);
set X =  {  H1(j) where j is Element of N : S1[j]  }  ;
  {  H1(j) where j is Element of N : S1[j]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th7;
 for G being Subset of R st G is open & x in G holds
{(sup D)} meets G
proof
let G be Subset of R; ::_thesis: ( G is open & x in G implies {(sup D)} meets G )
assume A2: G is open ; ::_thesis: ( not x in G or {(sup D)} meets G )
assume  x in G ; ::_thesis: {(sup D)} meets G
then reconsider G = G as a_neighborhood of x by A2, CONNSP_2:3;
A3: N is_often_in G by A1, WAYBEL_9:def_9;
now__::_thesis:_for_i_being_Element_of_N_holds_sup_D_in_G
let i be Element of N; ::_thesis: sup D in G
consider j1 being Element of N such that
 i <= j1 and
A4: N . j1 in G by A3, WAYBEL_0:def_12;
consider j2 being Element of N such that
A5: for k being Element of N st j2 <= k holds
N . j1 <= N . k by WAYBEL_0:11;
defpred S2[ Element of N] means $1 >= j2;
deffunc H2( Element of N) ->  Element of the carrier of R = N . $1;
set E =  {  H2(k) where k is Element of N : S2[k]  }  ;
A6:  {  H2(k) where k is Element of N : S2[k]  }  is Subset of R from DOMAIN_1:sch_8();
consider j9 being Element of N such that
A7: j9 >= j2 and
 j9 >= j2 by YELLOW_6:def_3;
 N . j9 in  {  H2(k) where k is Element of N : S2[k]  }  by A7;
then reconsider E9 =  {  H2(k) where k is Element of N : S2[k]  }  as non empty Subset of R by A6;
A8: ex_inf_of E9,R by WAYBEL_0:76;
 N . j1 is_<=_than E9
proof
let b be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not b in E9 or N . j1 <= b )
assume  b in E9 ; ::_thesis: N . j1 <= b
then  ex k being Element of N st
( b = N . k & k >= j2 ) ;
hence  N . j1 <= b by A5; ::_thesis: verum
end;
then A9: N . j1 <= "/\" (E9,R) by A8, YELLOW_0:31;
 for a being Element of R holds downarrow a = Cl {a} by Def2;
then A10: G is upper by A2, Th21;
then A11: "/\" (E9,R) in G by A4, A9, WAYBEL_0:def_20;
 "/\" (E9,R) in D ;
then  "/\" (E9,R) <= sup D by Th17;
hence  sup D in G by A10, A11, WAYBEL_0:def_20; ::_thesis: verum
end;
then A12: sup D in G ;
 sup D in {(sup D)} by TARSKI:def_1;
hence  {(sup D)} meets G by A12, XBOOLE_0:3; ::_thesis: verum
end;
then  x in Cl {(sup D)} by PRE_TOPC:24;
then  x in downarrow (sup D) by Def2;
hence  x <= lim_inf N by WAYBEL_0:17; ::_thesis: verum
end;
end;