:: WAYBEL11 semantic presentation

begin

Lm1:  for R, S being RelStr
for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
proof
let R, S be RelStr ; ::_thesis: for p, q being Element of R
for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p, q be Element of R; ::_thesis: for p9, q9 being Element of S st p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q holds
p9 <= q9
let p9, q9 be Element of S; ::_thesis: ( p = p9 & q = q9 & RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) & p <= q implies p9 <= q9 )
assume that
A1: p = p9 and
A2: q = q9 and
A3: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of S, the InternalRel of S #) ; ::_thesis: ( not p <= q or p9 <= q9 )
assume  p <= q ; ::_thesis: p9 <= q9
then  [p9,q9] in the InternalRel of S by A1, A2, A3, ORDERS_2:def_5;
hence  p9 <= q9 by ORDERS_2:def_5; ::_thesis: verum
end;

scheme :: WAYBEL11:sch 1
Irrel{ F1() ->  non empty set , F2() ->  non empty set , P1[ set ], F3( set ) ->  set , F4( set , set ) ->  set } :
  {  F3(u) where u is Element of F1() : P1[u]  }  =  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }
provided
A1: for i being Element of F2()
for u being Element of F1() holds F3(u) = F4(i,u)
proof
set A =  {  F3(u) where u is Element of F1() : P1[u]  }  ;
set B =  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  ;
thus   {  F3(u) where u is Element of F1() : P1[u]  }  c=  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  c=  {  F3(u) where u is Element of F1() : P1[u]  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  F3(u) where u is Element of F1() : P1[u]  }  or e in  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  )
set i = the Element of F2();
assume  e in  {  F3(u) where u is Element of F1() : P1[u]  }  ; ::_thesis: e in  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }
then consider u being Element of F1() such that
A2: e = F3(u) and
A3: P1[u] ;
 e = F4( the Element of F2(),u) by A1, A2;
hence  e in  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  by A3; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  or e in  {  F3(u) where u is Element of F1() : P1[u]  }  )
assume  e in  {  F4(i,v) where i is Element of F2(), v is Element of F1() : P1[v]  }  ; ::_thesis: e in  {  F3(u) where u is Element of F1() : P1[u]  }
then consider i being Element of F2(), u being Element of F1() such that
A4: e = F4(i,u) and
A5: P1[u] ;
 e = F3(u) by A1, A4;
hence  e in  {  F3(u) where u is Element of F1() : P1[u]  }  by A5; ::_thesis: verum
end;

theorem Th1: :: WAYBEL11:1
for L being complete LATTICE
for X, Y being Subset of L st Y is_coarser_than X holds
"/\" (X,L) <= "/\" (Y,L)
proof
let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st Y is_coarser_than X holds
"/\" (X,L) <= "/\" (Y,L)
let X, Y be Subset of L; ::_thesis: ( Y is_coarser_than X implies "/\" (X,L) <= "/\" (Y,L) )
assume A1: Y is_coarser_than X ; ::_thesis: "/\" (X,L) <= "/\" (Y,L)
 "/\" (X,L) is_<=_than Y
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in Y or "/\" (X,L) <= y )
assume  y in Y ; ::_thesis: "/\" (X,L) <= y
then consider x being Element of L such that
A2: x in X and
A3: x <= y by A1, YELLOW_4:def_2;
 "/\" (X,L) <= x by A2, YELLOW_2:22;
hence  "/\" (X,L) <= y by A3, YELLOW_0:def_2; ::_thesis: verum
end;
hence  "/\" (X,L) <= "/\" (Y,L) by YELLOW_0:33; ::_thesis: verum
end;

theorem Th2: :: WAYBEL11:2
for L being complete LATTICE
for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)
proof
let L be complete LATTICE; ::_thesis: for X, Y being Subset of L st X is_finer_than Y holds
"\/" (X,L) <= "\/" (Y,L)
let X, Y be Subset of L; ::_thesis: ( X is_finer_than Y implies "\/" (X,L) <= "\/" (Y,L) )
assume A1: X is_finer_than Y ; ::_thesis: "\/" (X,L) <= "\/" (Y,L)
 "\/" (Y,L) is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= "\/" (Y,L) )
assume  x in X ; ::_thesis: x <= "\/" (Y,L)
then consider y being Element of L such that
A2: y in Y and
A3: x <= y by A1, YELLOW_4:def_1;
 "\/" (Y,L) >= y by A2, YELLOW_2:22;
hence  x <= "\/" (Y,L) by A3, YELLOW_0:def_2; ::_thesis: verum
end;
hence  "\/" (X,L) <= "\/" (Y,L) by YELLOW_0:32; ::_thesis: verum
end;

theorem :: WAYBEL11:3
for T being RelStr
for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
proof
let T be RelStr ; ::_thesis: for A being upper Subset of T
for B being directed Subset of T holds A /\ B is directed
let A be upper Subset of T; ::_thesis: for B being directed Subset of T holds A /\ B is directed
let B be directed Subset of T; ::_thesis: A /\ B is directed
let x, y be Element of T; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in A /\ B or not y in A /\ B or ex b1 being Element of the carrier of T st
( b1 in A /\ B & x <= b1 & y <= b1 ) )
assume that
A1: x in A /\ B and
A2: y in A /\ B ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in A /\ B & x <= b1 & y <= b1 )
A3: x in B by A1, XBOOLE_0:def_4;
 y in B by A2, XBOOLE_0:def_4;
then consider z being Element of T such that
A4: z in B and
A5: x <= z and
A6: y <= z by A3, WAYBEL_0:def_1;
take  z ; ::_thesis: ( z in A /\ B & x <= z & y <= z )
 x in A by A1, XBOOLE_0:def_4;
then  z in A by A5, WAYBEL_0:def_20;
hence  z in A /\ B by A4, XBOOLE_0:def_4; ::_thesis: ( x <= z & y <= z )
thus  ( x <= z & y <= z ) by A5, A6; ::_thesis: verum
end;

registration
let T be non empty reflexive RelStr ;
cluster non empty finite directed for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is directed & b1 is finite )
proof
set x = the Element of T;
take  { the Element of T} ; ::_thesis: ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite )
thus  ( not { the Element of T} is empty & { the Element of T} is directed & { the Element of T} is finite ) by WAYBEL_0:5; ::_thesis: verum
end;
end;

theorem Th4: :: WAYBEL11:4
for T being with_suprema Poset
for D being non empty finite directed Subset of T holds sup D in D
proof
let T be reflexive transitive antisymmetric with_suprema RelStr ; ::_thesis: for D being non empty finite directed Subset of T holds sup D in D
let D be non empty finite directed Subset of T; ::_thesis: sup D in D
 D c= D ;
then reconsider E = D as finite Subset of D ;
consider x being Element of T such that
A1: x in D and
A2: x is_>=_than E by WAYBEL_0:1;
A3: for b being Element of T st D is_<=_than b holds
b >= x by A1, 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
A4: D is_<=_than c and
A5: for b being Element of T st D is_<=_than b holds
b >= c ; ::_thesis: c = x
A6: x >= c by A2, A5;
 c >= x by A1, A4, LATTICE3:def_9;
hence  c = x by A6, ORDERS_2:2; ::_thesis: verum
end;
then  ex_sup_of D,T by A2, A3, YELLOW_0:def_7;
hence  sup D in D by A1, A2, A3, YELLOW_0:def_9; ::_thesis: verum
end;

registration
cluster finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
existence
 ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is 1 -element & b1 is antisymmetric & b1 is with_suprema & b1 is with_infima & b1 is finite & b1 is strict )
proof
 0 in {0} by TARSKI:def_1;
then reconsider r = {[0,0]} as Relation of {0} by RELSET_1:3;
reconsider T = RelStr(# {0},r #) as non empty RelStr ;
take  T ; ::_thesis: ( T is reflexive & T is transitive & T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
thus  T is reflexive ::_thesis: ( T is transitive & T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
proof
let x be Element of T; :: according to YELLOW_0:def_1 ::_thesis: x <= x
 x = 0 by TARSKI:def_1;
then  [x,x] in {[0,0]} by TARSKI:def_1;
hence  x <= x by ORDERS_2:def_5; ::_thesis: verum
end;
then reconsider T9 = T as 1 -element reflexive RelStr ;
 T9 is transitive ;
hence  T is transitive ; ::_thesis: ( T is 1 -element & T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
thus  T is 1 -element ; ::_thesis: ( T is antisymmetric & T is with_suprema & T is with_infima & T is finite & T is strict )
 T9 is antisymmetric ;
hence  T is antisymmetric ; ::_thesis: ( T is with_suprema & T is with_infima & T is finite & T is strict )
 T9 is with_suprema ;
hence  T is with_suprema ; ::_thesis: ( T is with_infima & T is finite & T is strict )
 T9 is with_infima ;
hence  T is with_infima ; ::_thesis: ( T is finite & T is strict )
thus  T is finite ; ::_thesis: T is strict
thus  T is strict ; ::_thesis: verum
end;
end;

registration
let T be finite 1-sorted ;
cluster  ->  finite for Element of bool the carrier of T;
coherence
 for b1 being Subset of T holds b1 is finite ;
end;

registration
let R be RelStr ;
cluster empty  ->  lower upper for Element of bool the carrier of R;
coherence
 for b1 being Subset of R st b1 is empty holds
( b1 is lower & b1 is upper )
proof
let S be Subset of R; ::_thesis: ( S is empty implies ( S is lower & S is upper ) )
assume  S is empty ; ::_thesis: ( S is lower & S is upper )
then A1: S = {} R ;
hence  for x, y being Element of R st x in S & y <= x holds
y in S ; :: according to WAYBEL_0:def_19 ::_thesis: S is upper
thus  for x, y being Element of R st x in S & x <= y holds
y in S by A1; :: according to WAYBEL_0:def_20 ::_thesis: verum
end;
end;

registration
let R be 1 -element RelStr ;
cluster  ->  upper for Element of bool the carrier of R;
coherence
 for b1 being Subset of R holds b1 is upper
proof
let S be Subset of R; ::_thesis: S is upper
 ex x being Element of R st the carrier of R = {x} by TEX_1:def_1;
then  ( S = {} R or S = [#] R ) by ZFMISC_1:33;
hence  S is upper ; ::_thesis: verum
end;
end;

theorem Th5: :: WAYBEL11:5
for T being non empty RelStr
for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
proof
let T be non empty RelStr ; ::_thesis: for x being Element of T
for A being upper Subset of T st not x in A holds
A misses downarrow x
let x be Element of T; ::_thesis: for A being upper Subset of T st not x in A holds
A misses downarrow x
let A be upper Subset of T; ::_thesis: ( not x in A implies A misses downarrow x )
assume A1: not x in A ; ::_thesis: A misses downarrow x
assume  A meets downarrow x ; ::_thesis: contradiction
then consider y being set  such that
A2: y in A and
A3: y in downarrow x by XBOOLE_0:3;
reconsider y = y as Element of T by A2;
 y <= x by A3, WAYBEL_0:17;
hence  contradiction by A1, A2, WAYBEL_0:def_20; ::_thesis: verum
end;

theorem Th6: :: WAYBEL11:6
for T being non empty RelStr
for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
proof
let T be non empty RelStr ; ::_thesis: for x being Element of T
for A being lower Subset of T st x in A holds
downarrow x c= A
let x be Element of T; ::_thesis: for A being lower Subset of T st x in A holds
downarrow x c= A
let A be lower Subset of T; ::_thesis: ( x in A implies downarrow x c= A )
assume  x in A ; ::_thesis: downarrow x c= A
then  not x in A ` by XBOOLE_0:def_5;
then  A ` misses downarrow x by Th5;
then  A ` c= (downarrow x) ` by SUBSET_1:23;
hence  downarrow x c= A by SUBSET_1:12; ::_thesis: verum
end;

begin

definition
let T be non empty reflexive RelStr ;
let S be Subset of T;
attrS is inaccessible_by_directed_joins  means :Def1: :: WAYBEL11:def 1
 for D being non empty directed Subset of T st sup D in S holds
D meets S;
attrS is closed_under_directed_sups  means :Def2: :: WAYBEL11:def 2
 for D being non empty directed Subset of T st D c= S holds
sup D in S;
attrS is property(S)  means :Def3: :: WAYBEL11:def 3
 for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) );
end;

:: deftheorem Def1 defines inaccessible_by_directed_joins WAYBEL11:def_1_:_
 for T being non empty reflexive RelStr
for S being Subset of T holds
( S is inaccessible_by_directed_joins iff for D being non empty directed Subset of T st sup D in S holds
D meets S );

:: deftheorem Def2 defines closed_under_directed_sups WAYBEL11:def_2_:_
 for T being non empty reflexive RelStr
for S being Subset of T holds
( S is closed_under_directed_sups iff for D being non empty directed Subset of T st D c= S holds
sup D in S );

:: deftheorem Def3 defines property(S) WAYBEL11:def_3_:_
 for T being non empty reflexive RelStr
for S being Subset of T holds
( S is property(S) iff for D being non empty directed Subset of T st sup D in S holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) );

notation
let T be non empty reflexive RelStr ;
let S be Subset of T;
synonym  inaccessible S for  inaccessible_by_directed_joins ;
synonym  directly_closed S for  closed_under_directed_sups ;
end;

registration
let T be non empty reflexive RelStr ;
cluster empty  ->  directly_closed property(S) for Element of bool the carrier of T;
coherence
 for b1 being Subset of T st b1 is empty holds
( b1 is property(S) & b1 is directly_closed )
proof
let S be Subset of T; ::_thesis: ( S is empty implies ( S is property(S) & S is directly_closed ) )
assume  S is empty ; ::_thesis: ( S is property(S) & S is directly_closed )
then A1: S = {} T ;
 for D being non empty directed Subset of T st sup D in {} T holds
ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in {} T ) ) ;
hence  S is property(S) by A1, Def3; ::_thesis: S is directly_closed
thus  for D being non empty directed Subset of T st D c= S holds
sup D in S by A1; :: according to WAYBEL11:def_2 ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
cluster directly_closed property(S) for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( b1 is property(S) & b1 is directly_closed )
proof
take  {} T ; ::_thesis: ( {} T is property(S) & {} T is directly_closed )
thus  ( {} T is property(S) & {} T is directly_closed ) ; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
let S be property(S) Subset of T;
clusterS `  ->  directly_closed ;
coherence
 S ` is closed_under_directed_sups
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` )
assume A1: D c= S ` ; ::_thesis: sup D in S `
assume  not sup D in S ` ; ::_thesis: contradiction
then  sup D in S by XBOOLE_0:def_5;
then consider y being Element of T such that
A2: y in D and
A3: for x being Element of T st x in D & x >= y holds
x in S by Def3;
 y <= y ;
then  y in S by A2, A3;
then  D /\ S <> {} by A2, XBOOLE_0:def_4;
then  D meets S by XBOOLE_0:def_7;
hence  contradiction by A1, SUBSET_1:23; ::_thesis: verum
end;
end;

definition
let T be non empty reflexive TopRelStr ;
attrT is Scott  means :Def4: :: WAYBEL11:def 4
 for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) );
end;

:: deftheorem Def4 defines Scott WAYBEL11:def_4_:_
 for T being non empty reflexive TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) );

registration
let T be non empty finite reflexive transitive antisymmetric with_suprema RelStr ;
cluster  ->  inaccessible for Element of bool the carrier of T;
coherence
 for b1 being Subset of T holds b1 is inaccessible
proof
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: ( sup D in S implies D meets S )
assume A1: sup D in S ; ::_thesis: D meets S
 sup D in D by Th4;
hence  D meets S by A1, XBOOLE_0:3; ::_thesis: verum
end;
end;

definition
let T be non empty finite reflexive transitive antisymmetric with_suprema TopRelStr ;
redefine attr T is Scott  means :: WAYBEL11:def 5
 for S being Subset of T holds
( S is open iff S is upper );
compatibility
 ( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) )
proof
thus  ( T is Scott implies for S being Subset of T holds
( S is open iff S is upper ) ) by Def4; ::_thesis: ( ( for S being Subset of T holds
( S is open iff S is upper ) ) implies T is Scott )
assume A1: for S being Subset of T holds
( S is open iff S is upper ) ; ::_thesis: T is Scott
let S be Subset of T; :: according to WAYBEL11:def_4 ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) )
thus  ( S is open iff ( S is inaccessible & S is upper ) ) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines Scott WAYBEL11:def_5_:_
 for T being non empty finite reflexive transitive antisymmetric with_suprema TopRelStr holds
( T is Scott iff for S being Subset of T holds
( S is open iff S is upper ) );

registration
cluster non empty 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete strict Scott for TopRelStr ;
existence
 ex b1 being TopLattice st
( b1 is complete & b1 is strict & b1 is 1 -element & b1 is Scott )
proof
set T = the finite 1 -element discrete reflexive strict TopRelStr ;
take  the finite 1 -element discrete reflexive strict TopRelStr ; ::_thesis: ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element & the finite 1 -element discrete reflexive strict TopRelStr is Scott )
thus  ( the finite 1 -element discrete reflexive strict TopRelStr is complete & the finite 1 -element discrete reflexive strict TopRelStr is strict & the finite 1 -element discrete reflexive strict TopRelStr is 1 -element ) ; ::_thesis: the finite 1 -element discrete reflexive strict TopRelStr is Scott
let S be Subset of the finite 1 -element discrete reflexive strict TopRelStr ; :: according to WAYBEL11:def_5 ::_thesis: ( S is open iff S is upper )
thus  ( S is open iff S is upper ) by TDLAT_3:15; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
cluster [#] T ->  inaccessible directly_closed ;
coherence
 ( [#] T is closed_under_directed_sups & [#] T is inaccessible_by_directed_joins )
proof
thus  [#] T is directly_closed ::_thesis: [#] T is inaccessible_by_directed_joins
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= [#] T implies sup D in [#] T )
assume  D c= [#] T ; ::_thesis: sup D in [#] T
thus  sup D in [#] T ; ::_thesis: verum
end;
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in [#] T implies D meets [#] T )
assume  sup D in [#] T ; ::_thesis: D meets [#] T
 ex p being Element of T st p in D by SUBSET_1:4;
hence  D meets [#] T by XBOOLE_0:3; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
cluster lower upper inaccessible directly_closed for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( b1 is directly_closed & b1 is lower & b1 is inaccessible & b1 is upper )
proof
take  [#] T ; ::_thesis: ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper )
thus  ( [#] T is directly_closed & [#] T is lower & [#] T is inaccessible & [#] T is upper ) ; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
let S be inaccessible Subset of T;
clusterS `  ->  directly_closed ;
coherence
 S ` is closed_under_directed_sups
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= S ` implies sup D in S ` )
assume  D c= S ` ; ::_thesis: sup D in S `
then  D misses S by SUBSET_1:23;
then  not sup D in S by Def1;
hence  sup D in S ` by XBOOLE_0:def_5; ::_thesis: verum
end;
end;

registration
let T be non empty reflexive RelStr ;
let S be directly_closed Subset of T;
clusterS `  ->  inaccessible ;
coherence
 S ` is inaccessible_by_directed_joins
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S ` implies D meets S ` )
assume  sup D in S ` ; ::_thesis: D meets S `
then  not sup D in S by XBOOLE_0:def_5;
then  not D c= (S `) ` by Def2;
hence  D meets S ` by SUBSET_1:23; ::_thesis: verum
end;
end;

theorem Th7: :: WAYBEL11:7
for T being non empty reflexive transitive up-complete Scott TopRelStr
for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )
proof
let T be non empty reflexive transitive up-complete Scott TopRelStr ; ::_thesis: for S being Subset of T holds
( S is closed iff ( S is directly_closed & S is lower ) )
let S be Subset of T; ::_thesis: ( S is closed iff ( S is directly_closed & S is lower ) )
hereby  ::_thesis: ( S is directly_closed & S is lower implies S is closed )
assume  S is closed ; ::_thesis: ( S is directly_closed & S is lower )
then  S ` is open by TOPS_1:3;
then reconsider A = S ` as upper inaccessible Subset of T by Def4;
 ( A ` is directly_closed & A ` is lower ) ;
hence  ( S is directly_closed & S is lower ) ; ::_thesis: verum
end;
assume  ( S is directly_closed & S is lower ) ; ::_thesis: S is closed
then reconsider S = S as lower directly_closed Subset of T ;
 S ` is open by Def4;
hence  S is closed by TOPS_1:3; ::_thesis: verum
end;

theorem Th8: :: WAYBEL11:8
for T being non empty reflexive transitive antisymmetric up-complete TopRelStr
for x being Element of T holds downarrow x is directly_closed
proof
let T be non empty reflexive transitive antisymmetric up-complete TopRelStr ; ::_thesis: for x being Element of T holds downarrow x is directly_closed
let x be Element of T; ::_thesis: downarrow x is directly_closed
 downarrow x is directly_closed
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_2 ::_thesis: ( D c= downarrow x implies sup D in downarrow x )
assume A1: D c= downarrow x ; ::_thesis: sup D in downarrow x
 ex a being Element of T st
( a is_>=_than D & ( for b being Element of T st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def_39;
then A2: ex_sup_of D,T by YELLOW_0:15;
 x is_>=_than D
proof
let b be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not b in D or b <= x )
assume  b in D ; ::_thesis: b <= x
hence  b <= x by A1, WAYBEL_0:17; ::_thesis: verum
end;
then  sup D <= x by A2, YELLOW_0:30;
hence  sup D in downarrow x by WAYBEL_0:17; ::_thesis: verum
end;
hence  downarrow x is directly_closed ; ::_thesis: verum
end;

theorem Th9: :: WAYBEL11:9
for T being complete Scott TopLattice
for x being Element of T holds Cl {x} = downarrow x
proof
let T be complete Scott TopLattice; ::_thesis: for x being Element of T holds Cl {x} = downarrow x
let x be Element of T; ::_thesis: Cl {x} = downarrow x
 downarrow x is directly_closed by Th8;
then A1: downarrow x is closed by Th7;
 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_T_st_{x}_c=_C_&_C_is_closed_holds_
downarrow_x_c=_C
let C be Subset of T; ::_thesis: ( {x} c= C & C is closed implies downarrow x c= C )
assume A3: {x} c= C ; ::_thesis: ( C is closed implies downarrow x c= C )
reconsider D = C as Subset of T ;
assume  C is closed ; ::_thesis: downarrow x c= C
then A4: D is lower by Th7;
 x in C by A3, ZFMISC_1:31;
hence  downarrow x c= C by A4, Th6; ::_thesis: verum
end;
hence  Cl {x} = downarrow x by A1, A2, YELLOW_8:8; ::_thesis: verum
end;

theorem :: WAYBEL11:10
for T being complete Scott TopLattice holds T is T_0-TopSpace
proof
let T be complete Scott TopLattice; ::_thesis: T is T_0-TopSpace
now__::_thesis:_for_x,_y_being_Point_of_T_st_x_<>_y_holds_
Cl_{x}_<>_Cl_{y}
let x, y be Point of T; ::_thesis: ( x <> y implies Cl {x} <> Cl {y} )
reconsider x9 = x, y9 = y as Element of T ;
A1: Cl {x9} = downarrow x9 by Th9;
A2: Cl {y9} = downarrow y9 by Th9;
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;

theorem Th11: :: WAYBEL11:11
for T being non empty reflexive transitive antisymmetric up-complete Scott TopRelStr
for x being Element of T holds downarrow x is closed
proof
let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; ::_thesis: for x being Element of T holds downarrow x is closed
let x be Element of T; ::_thesis: downarrow x is closed
 ( downarrow x is directly_closed & downarrow x is lower ) by Th8;
hence  downarrow x is closed by Th7; ::_thesis: verum
end;

theorem Th12: :: WAYBEL11:12
for T being up-complete Scott TopLattice
for x being Element of T holds (downarrow x) ` is open
proof
let T be up-complete Scott TopLattice; ::_thesis: for x being Element of T holds (downarrow x) ` is open
let x be Element of T; ::_thesis: (downarrow x) ` is open
 downarrow x is closed by Th11;
hence  (downarrow x) ` is open ; ::_thesis: verum
end;

theorem Th13: :: WAYBEL11:13
for T being up-complete Scott TopLattice
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 T be up-complete Scott TopLattice; ::_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 open by Th12;
then A2: Int ((downarrow x) `) = (downarrow x) ` by TOPS_1:23;
 A misses downarrow x by A1, Th5;
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 :: WAYBEL11:14
for T being complete Scott TopLattice
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 T be complete Scott TopLattice; ::_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, Th13;
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 :: WAYBEL11:15
for T being Scott TopLattice
for S being Subset of T holds
( S is open iff ( S is upper & S is property(S) ) )
proof
let T be Scott TopLattice; ::_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 A2: S is upper by Def4; ::_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: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A3: sup D in S ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
 S is inaccessible by A1, Def4;
then  S meets D by A3, Def1;
then consider y being set  such that
A4: y in S and
A5: y in D by XBOOLE_0:3;
reconsider y = y as Element of T by A4;
take  y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) )
thus  ( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) by A2, A4, A5, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
assume that
A6: S is upper and
A7: 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: ( sup D in S implies D meets S )
assume  sup D in S ; ::_thesis: D meets S
then consider y being Element of T such that
A8: y in D and
A9: for x being Element of T st x in D & x >= y holds
x in S by A7, Def3;
 y >= y by YELLOW_0:def_1;
then  y in S by A8, A9;
hence  D meets S by A8, XBOOLE_0:3; ::_thesis: verum
end;
hence  S is open by A6, Def4; ::_thesis: verum
end;

registration
let T be complete TopLattice;
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: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A2: sup D in S ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x 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 x being Element of T st x in D & x >= y holds
x in S ) )
thus  y in D by A3; ::_thesis: for x being Element of T st x in D & x >= y holds
x in S
let x be Element of T; ::_thesis: ( x in D & x >= y implies x in S )
assume that
A4: x in D and
 x >= y ; ::_thesis: x in S
 x <= sup D by A4, YELLOW_2:22;
hence  x in S by A1, A2, WAYBEL_0:def_19; ::_thesis: verum
end;
end;

Lm2:  for T being non empty reflexive TopRelStr holds [#] T is property(S)
proof
let T be non empty reflexive TopRelStr ; ::_thesis: [#] T is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in [#] T implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) ) )
assume  sup D in [#] T ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) )
consider y being Element of T such that
A1: y in D by SUBSET_1:4;
take  y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in [#] T ) )
thus  y in D by A1; ::_thesis: for x being Element of T st x in D & x >= y holds
x in [#] T
let x be Element of T; ::_thesis: ( x in D & x >= y implies x in [#] T )
assume that
 x in D and
 x >= y ; ::_thesis: x in [#] T
thus  x in [#] T ; ::_thesis: verum
end;

theorem :: WAYBEL11:16
for T being non empty reflexive transitive TopRelStr st the topology of T =  {  S where S is Subset of T : S is property(S)  }  holds
T is TopSpace-like
proof
let T be non empty reflexive transitive TopRelStr ; ::_thesis: ( the topology of T =  {  S where S is Subset of T : S is property(S)  }  implies T is TopSpace-like )
assume A1: the topology of T =  {  S where S is Subset of T : S is property(S)  }  ; ::_thesis: T is TopSpace-like
 [#] T is property(S) by Lm2;
hence  the carrier of T in the topology of T by A1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
hereby  ::_thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T )
let a be Subset-Family of T; ::_thesis: ( a c= the topology of T implies union a in the topology of T )
assume A2: a c= the topology of T ; ::_thesis: union a in the topology of T
 union a is property(S)
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in union a implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) ) )
assume  sup D in union a ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) )
then consider x being set  such that
A3: sup D in x and
A4: x in a by TARSKI:def_4;
 x in the topology of T by A2, A4;
then consider X being Subset of T such that
A5: x = X and
A6: X is property(S) by A1;
consider y being Element of T such that
A7: y in D and
A8: for x being Element of T st x in D & x >= y holds
x in X by A3, A5, A6, Def3;
take  y ; ::_thesis: ( y in D & ( for x being Element of T st x in D & x >= y holds
x in union a ) )
thus  y in D by A7; ::_thesis: for x being Element of T st x in D & x >= y holds
x in union a
let u be Element of T; ::_thesis: ( u in D & u >= y implies u in union a )
assume that
A9: u in D and
A10: u >= y ; ::_thesis: u in union a
 u in X by A8, A9, A10;
hence  u in union a by A4, A5, TARSKI:def_4; ::_thesis: verum
end;
hence  union a in the topology of T by A1; ::_thesis: verum
end;
let a, b be Subset of T; ::_thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
assume  a in the topology of T ; ::_thesis: ( not b in the topology of T or a /\ b in the topology of T )
then consider A being Subset of T such that
A11: a = A and
A12: A is property(S) by A1;
assume  b in the topology of T ; ::_thesis: a /\ b in the topology of T
then consider B being Subset of T such that
A13: b = B and
A14: B is property(S) by A1;
 A /\ B is property(S)
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_3 ::_thesis: ( sup D in A /\ B implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) ) )
assume A15: sup D in A /\ B ; ::_thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in A /\ B ) )
then  sup D in A by XBOOLE_0:def_4;
then consider x being Element of T such that
A16: x in D and
A17: for z being Element of T st z in D & z >= x holds
z in A by A12, Def3;
 sup D in B by A15, XBOOLE_0:def_4;
then consider y being Element of T such that
A18: y in D and
A19: for z being Element of T st z in D & z >= y holds
z in B by A14, Def3;
consider z being Element of T such that
A20: z in D and
A21: x <= z and
A22: y <= z by A16, A18, WAYBEL_0:def_1;
take  z ; ::_thesis: ( z in D & ( for x being Element of T st x in D & x >= z holds
x in A /\ B ) )
thus  z in D by A20; ::_thesis: for x being Element of T st x in D & x >= z holds
x in A /\ B
let u be Element of T; ::_thesis: ( u in D & u >= z implies u in A /\ B )
assume A23: u in D ; ::_thesis: ( not u >= z or u in A /\ B )
assume A24: u >= z ; ::_thesis: u in A /\ B
then  u >= x by A21, YELLOW_0:def_2;
then A25: u in A by A17, A23;
 u >= y by A22, A24, YELLOW_0:def_2;
then  u in B by A19, A23;
hence  u in A /\ B by A25, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  a /\ b in the topology of T by A1, A11, A13; ::_thesis: verum
end;

begin


definition
let R be non empty RelStr ;
let N be net of R;
func lim_inf N ->  Element of R equals :: WAYBEL11:def 6
 "\/" ( {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ,R);
correctness
coherence
"\/" ( {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ,R) is Element of R;
;
end;

:: deftheorem  defines lim_inf WAYBEL11:def_6_:_
 for R being non empty RelStr
for N being net of R holds lim_inf N = "\/" ( {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ,R);

definition
let R be non empty reflexive RelStr ;
let N be net of R;
let p be Element of R;
predp is_S-limit_of N means :Def7: :: WAYBEL11:def 7
p <= lim_inf N;
end;

:: deftheorem Def7 defines is_S-limit_of WAYBEL11:def_7_:_
 for R being non empty reflexive RelStr
for N being net of R
for p being Element of R holds
( p is_S-limit_of N iff p <= lim_inf N );

definition
let R be non empty reflexive RelStr ;
func Scott-Convergence R ->  Convergence-Class of R means :Def8: :: WAYBEL11:def 8
 for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it iff p is_S-limit_of N );
existence
 ex b1 being Convergence-Class of R st
for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N )
proof
defpred S1[ set , Element of R] means  ex N being strict net of R st
( N = $1 & $2 is_S-limit_of N );
consider C being Relation of (NetUniv R), the carrier of R such that
A1: for x being Element of NetUniv R
for y being Element of R holds
( [x,y] in C iff S1[x,y] ) from RELSET_1:sch_2();
reconsider C = C as Convergence-Class of R by YELLOW_6:def_18;
take  C ; ::_thesis: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let N be strict net of R; ::_thesis: ( N in NetUniv R implies for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N ) )
assume A2: N in NetUniv R ; ::_thesis: for p being Element of R holds
( [N,p] in C iff p is_S-limit_of N )
let p be Element of R; ::_thesis: ( [N,p] in C iff p is_S-limit_of N )
hereby  ::_thesis: ( p is_S-limit_of N implies [N,p] in C )
assume  [N,p] in C ; ::_thesis: p is_S-limit_of N
then  ex M being strict net of R st
( M = N & p is_S-limit_of M ) by A1, A2;
hence  p is_S-limit_of N ; ::_thesis: verum
end;
thus  ( p is_S-limit_of N implies [N,p] in C ) by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Convergence-Class of R st ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) ) holds
b1 = b2
proof
let it1, it2 be Convergence-Class of R; ::_thesis: ( ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) ) & ( for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ) implies it1 = it2 )
assume that
A3: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it1 iff p is_S-limit_of N ) and
A4: for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in it2 iff p is_S-limit_of N ) ; ::_thesis: it1 = it2
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in it1 or [x,y] in it2 ) & ( not [x,y] in it2 or [x,y] in it1 ) )
A5: it1 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
A6: it2 c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
hereby  ::_thesis: ( not [x,y] in it2 or [x,y] in it1 )
assume A7: [x,y] in it1 ; ::_thesis: [x,y] in it2
then A8: x in NetUniv R by A5, ZFMISC_1:87;
then consider N being strict net of R such that
A9: N = x and
 the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11;
reconsider p = y as Element of R by A5, A7, ZFMISC_1:87;
 p is_S-limit_of N by A3, A7, A8, A9;
hence  [x,y] in it2 by A4, A8, A9; ::_thesis: verum
end;
assume A10: [x,y] in it2 ; ::_thesis: [x,y] in it1
then A11: x in NetUniv R by A6, ZFMISC_1:87;
then consider N being strict net of R such that
A12: N = x and
 the carrier of N in the_universe_of the carrier of R by YELLOW_6:def_11;
reconsider p = y as Element of R by A6, A10, ZFMISC_1:87;
 p is_S-limit_of N by A4, A10, A11, A12;
hence  [x,y] in it1 by A3, A11, A12; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Scott-Convergence WAYBEL11:def_8_:_
 for R being non empty reflexive RelStr
for b2 being Convergence-Class of R holds
( b2 = Scott-Convergence R iff for N being strict net of R st N in NetUniv R holds
for p being Element of R holds
( [N,p] in b2 iff p is_S-limit_of N ) );

theorem :: WAYBEL11:17
for R being complete LATTICE
for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
proof
let R be complete LATTICE; ::_thesis: for N being net of R
for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let N be net of R; ::_thesis: for p, q being Element of R st p is_S-limit_of N & N is_eventually_in downarrow q holds
p <= q
let p, q be Element of R; ::_thesis: ( p is_S-limit_of N & N is_eventually_in downarrow q implies p <= q )
assume that
A1: p <= lim_inf N and
A2: N is_eventually_in downarrow q ; :: according to WAYBEL11:def_7 ::_thesis: p <= q
consider j0 being Element of N such that
A3: for i being Element of N st j0 <= i holds
N . i in downarrow q by A2, WAYBEL_0:def_11;
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ;
reconsider q9 = q as Element of R ;
 q9 is_>=_than  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
proof
let x be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  or x <= q9 )
assume  x in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ; ::_thesis: x <= q9
then consider j1 being Element of N such that
A4: x = "/\" ( {  (N . i) where i is Element of N : i >= j1  }  ,R) ;
set Y =  {  (N . i) where i is Element of N : i >= j1  }  ;
reconsider j1 = j1 as Element of N ;
consider j2 being Element of N such that
A5: j2 >= j0 and
A6: j2 >= j1 by YELLOW_6:def_3;
 N . j2 in  {  (N . i) where i is Element of N : i >= j1  }  by A6;
then A7: x <= N . j2 by A4, YELLOW_2:22;
 N . j2 in downarrow q by A3, A5;
then  N . j2 <= q9 by WAYBEL_0:17;
hence  x <= q9 by A7, YELLOW_0:def_2; ::_thesis: verum
end;
then  lim_inf N <= q9 by YELLOW_0:32;
hence  p <= q by A1, YELLOW_0:def_2; ::_thesis: verum
end;

theorem Th18: :: WAYBEL11:18
for R being complete LATTICE
for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
proof
let R be complete LATTICE; ::_thesis: for N being net of R
for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let N be net of R; ::_thesis: for p, q being Element of R st N is_eventually_in uparrow q holds
lim_inf N >= q
let p, q be Element of R; ::_thesis: ( N is_eventually_in uparrow q implies lim_inf N >= q )
assume  N is_eventually_in uparrow q ; ::_thesis: lim_inf N >= q
then consider j0 being Element of N such that
A1: for i being Element of N st j0 <= i holds
N . i in uparrow q by WAYBEL_0:def_11;
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ;
set Y =  {  (N . i) where i is Element of N : i >= j0  }  ;
reconsider q9 = q as Element of R ;
 "/\" ( {  (N . i) where i is Element of N : i >= j0  }  ,R) in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ;
then A2: lim_inf N >= "/\" ( {  (N . i) where i is Element of N : i >= j0  }  ,R) by YELLOW_2:22;
 q9 is_<=_than  {  (N . i) where i is Element of N : i >= j0  }
proof
let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in  {  (N . i) where i is Element of N : i >= j0  }  or q9 <= y )
assume  y in  {  (N . i) where i is Element of N : i >= j0  }  ; ::_thesis: q9 <= y
then consider i1 being Element of N such that
A3: y = N . i1 and
A4: i1 >= j0 ;
reconsider i19 = i1 as Element of N ;
 N . i19 in uparrow q by A1, A4;
hence  q9 <= y by A3, WAYBEL_0:18; ::_thesis: verum
end;
then  "/\" ( {  (N . i) where i is Element of N : i >= j0  }  ,R) >= q9 by YELLOW_0:33;
hence  lim_inf N >= q by A2, YELLOW_0:def_2; ::_thesis: verum
end;

definition
let R be non empty reflexive RelStr ;
let N be non empty NetStr over R;
redefine attr N is monotone  means :Def9: :: WAYBEL11:def 9
 for i, j being Element of N st i <= j holds
N . i <= N . j;
compatibility
 ( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j )
proof
hereby  ::_thesis: ( ( for i, j being Element of N st i <= j holds
N . i <= N . j ) implies N is monotone )
assume  N is monotone ; ::_thesis: for i, j being Element of N st i <= j holds
N . i <= N . j
then A1: netmap (N,R) is monotone by WAYBEL_0:def_9;
let i, j be Element of N; ::_thesis: ( i <= j implies N . i <= N . j )
assume  i <= j ; ::_thesis: N . i <= N . j
hence  N . i <= N . j by A1, WAYBEL_1:def_2; ::_thesis: verum
end;
assume A2: for i, j being Element of N st i <= j holds
N . i <= N . j ; ::_thesis: N is monotone
 netmap (N,R) is monotone
proof
let x, y be Element of N; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap (N,R)) . x <= (netmap (N,R)) . y )
A3: (netmap (N,R)) . x = N . x ;
A4: (netmap (N,R)) . y = N . y ;
assume  x <= y ; ::_thesis: (netmap (N,R)) . x <= (netmap (N,R)) . y
hence  (netmap (N,R)) . x <= (netmap (N,R)) . y by A2, A3, A4; ::_thesis: verum
end;
hence  N is monotone by WAYBEL_0:def_9; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines monotone WAYBEL11:def_9_:_
 for R being non empty reflexive RelStr
for N being non empty NetStr over R holds
( N is monotone iff for i, j being Element of N st i <= j holds
N . i <= N . j );

definition
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
func Net-Str (S,f) ->  non empty strict NetStr over R means :Def10: :: WAYBEL11:def 10
( the carrier of it = S & the mapping of it = f & ( for i, j being Element of it holds
( i <= j iff it . i <= it . j ) ) );
existence
 ex b1 being non empty strict NetStr over R st
( the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) )
proof
defpred S1[ Element of S, Element of S] means f . $1 <= f . $2;
consider R being Relation of S,S such that
A1: for x, y being Element of S holds
( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2();
take N = NetStr(# S,R,f #); ::_thesis: ( the carrier of N = S & the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus  the carrier of N = S ; ::_thesis: ( the mapping of N = f & ( for i, j being Element of N holds
( i <= j iff N . i <= N . j ) ) )
thus  the mapping of N = f ; ::_thesis: for i, j being Element of N holds
( i <= j iff N . i <= N . j )
let i, j be Element of N; ::_thesis: ( i <= j iff N . i <= N . j )
reconsider x = i, y = j as Element of S ;
 ( [x,y] in the InternalRel of N iff f . x <= f . y ) by A1;
hence  ( i <= j iff N . i <= N . j ) by ORDERS_2:def_5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being non empty strict NetStr over R st the carrier of b1 = S & the mapping of b1 = f & ( for i, j being Element of b1 holds
( i <= j iff b1 . i <= b1 . j ) ) & the carrier of b2 = S & the mapping of b2 = f & ( for i, j being Element of b2 holds
( i <= j iff b2 . i <= b2 . j ) ) holds
b1 = b2
proof
let it1, it2 be non empty strict NetStr over R; ::_thesis: ( the carrier of it1 = S & the mapping of it1 = f & ( for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) ) & the carrier of it2 = S & the mapping of it2 = f & ( for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ) implies it1 = it2 )
assume that
A2: the carrier of it1 = S and
A3: the mapping of it1 = f and
A4: for i, j being Element of it1 holds
( i <= j iff it1 . i <= it1 . j ) and
A5: the carrier of it2 = S and
A6: the mapping of it2 = f and
A7: for i, j being Element of it2 holds
( i <= j iff it2 . i <= it2 . j ) ; ::_thesis: it1 = it2
 the InternalRel of it1 = the InternalRel of it2
proof
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in the InternalRel of it1 or [x,y] in the InternalRel of it2 ) & ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 ) )
hereby  ::_thesis: ( not [x,y] in the InternalRel of it2 or [x,y] in the InternalRel of it1 )
assume A8: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2
then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it2 by A2, A5, A8, ZFMISC_1:87;
A9: it1 . i = it2 . i9 by A3, A6;
A10: it1 . j = it2 . j9 by A3, A6;
 i <= j by A8, ORDERS_2:def_5;
then  it2 . i9 <= it2 . j9 by A4, A9, A10;
then  i9 <= j9 by A7;
hence  [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum
end;
assume A11: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1
then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87;
reconsider i9 = x, j9 = y as Element of it1 by A2, A5, A11, ZFMISC_1:87;
A12: it2 . i = it1 . i9 by A3, A6;
A13: it2 . j = it1 . j9 by A3, A6;
 i <= j by A11, ORDERS_2:def_5;
then  it1 . i9 <= it1 . j9 by A7, A12, A13;
then  i9 <= j9 by A4;
hence  [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum
end;
hence  it1 = it2 by A2, A3, A5, A6; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines Net-Str WAYBEL11:def_10_:_
 for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R
for b4 being non empty strict NetStr over R holds
( b4 = Net-Str (S,f) iff ( the carrier of b4 = S & the mapping of b4 = f & ( for i, j being Element of b4 holds
( i <= j iff b4 . i <= b4 . j ) ) ) );

theorem Th19: :: WAYBEL11:19
for L being non empty 1-sorted
for N being non empty NetStr over L holds rng the mapping of N =  {  (N . i) where i is Element of N : verum  }
proof
let L be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over L holds rng the mapping of N =  {  (N . i) where i is Element of N : verum  }
let N be non empty NetStr over L; ::_thesis: rng the mapping of N =  {  (N . i) where i is Element of N : verum  }
set X =  {  (N . i) where i is Element of N : verum  }  ;
A1: the carrier of N = dom the mapping of N by FUNCT_2:def_1;
thus  rng the mapping of N c=  {  (N . i) where i is Element of N : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (N . i) where i is Element of N : verum  }  c= rng the mapping of N
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng the mapping of N or e in  {  (N . i) where i is Element of N : verum  }  )
assume  e in rng the mapping of N ; ::_thesis: e in  {  (N . i) where i is Element of N : verum  }
then consider u being set  such that
A2: u in dom the mapping of N and
A3: e = the mapping of N . u by FUNCT_1:def_3;
reconsider u = u as Element of N by A2;
 e = N . u by A3;
hence  e in  {  (N . i) where i is Element of N : verum  }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (N . i) where i is Element of N : verum  }  or e in rng the mapping of N )
assume  e in  {  (N . i) where i is Element of N : verum  }  ; ::_thesis: e in rng the mapping of N
then  ex i being Element of N st e = N . i ;
hence  e in rng the mapping of N by A1, FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th20: :: WAYBEL11:20
for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
proof
let R be non empty RelStr ; ::_thesis: for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed
let f be Function of S, the carrier of R; ::_thesis: ( rng f is directed implies Net-Str (S,f) is directed )
assume A1: rng f is directed ; ::_thesis: Net-Str (S,f) is directed
set N = Net-Str (S,f);
let x, y be Element of (Net-Str (S,f)); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str (S,f)) st
( x <= b1 & y <= b1 )
 f = the mapping of (Net-Str (S,f)) by Def10;
then A2: rng f =  {  ((Net-Str (S,f)) . i) where i is Element of (Net-Str (S,f)) : verum  }  by Th19;
then A3: (Net-Str (S,f)) . x in rng f ;
 (Net-Str (S,f)) . y in rng f by A2;
then consider p being Element of R such that
A4: p in rng f and
A5: (Net-Str (S,f)) . x <= p and
A6: (Net-Str (S,f)) . y <= p by A1, A3, WAYBEL_0:def_1;
consider z being set  such that
A7: z in dom f and
A8: p = f . z by A4, FUNCT_1:def_3;
reconsider z = z as Element of (Net-Str (S,f)) by A7, Def10;
take  z ; ::_thesis: ( x <= z & y <= z )
 p = (Net-Str (S,f)) . z by A8, Def10;
hence  ( x <= z & y <= z ) by A5, A6, Def10; ::_thesis: verum
end;

registration
let R be non empty RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) ->  non empty strict monotone ;
coherence
 Net-Str (S,f) is monotone
proof
set N = Net-Str (S,f);
 netmap ((Net-Str (S,f)),R) is monotone
proof
let x, y be Element of (Net-Str (S,f)); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y )
A1: (netmap ((Net-Str (S,f)),R)) . x = (Net-Str (S,f)) . x ;
A2: (netmap ((Net-Str (S,f)),R)) . y = (Net-Str (S,f)) . y ;
assume  x <= y ; ::_thesis: (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y
hence  (netmap ((Net-Str (S,f)),R)) . x <= (netmap ((Net-Str (S,f)),R)) . y by A1, A2, Def10; ::_thesis: verum
end;
hence  Net-Str (S,f) is monotone by WAYBEL_0:def_9; ::_thesis: verum
end;
end;

registration
let R be non empty transitive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) ->  non empty transitive strict ;
coherence
 Net-Str (S,f) is transitive
proof
set N = Net-Str (S,f);
let x, y, z be Element of (Net-Str (S,f)); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
A1: x <= y and
A2: y <= z ; ::_thesis: x <= z
A3: (Net-Str (S,f)) . x <= (Net-Str (S,f)) . y by A1, Def10;
 (Net-Str (S,f)) . y <= (Net-Str (S,f)) . z by A2, Def10;
then  (Net-Str (S,f)) . x <= (Net-Str (S,f)) . z by A3, YELLOW_0:def_2;
hence  x <= z by Def10; ::_thesis: verum
end;
end;

registration
let R be non empty reflexive RelStr ;
let S be non empty set ;
let f be Function of S, the carrier of R;
cluster Net-Str (S,f) ->  non empty reflexive strict ;
coherence
 Net-Str (S,f) is reflexive
proof
let x be Element of (Net-Str (S,f)); :: according to YELLOW_0:def_1 ::_thesis: x <= x
 (Net-Str (S,f)) . x <= (Net-Str (S,f)) . x ;
hence  x <= x by Def10; ::_thesis: verum
end;
end;

theorem Th21: :: WAYBEL11:21
for R being non empty transitive RelStr
for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
proof
let R be non empty transitive RelStr ; ::_thesis: for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let S be non empty set ; ::_thesis: for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R
let f be Function of S, the carrier of R; ::_thesis: ( S c= the carrier of R & Net-Str (S,f) is directed implies Net-Str (S,f) in NetUniv R )
assume that
A1: S c= the carrier of R and
A2: Net-Str (S,f) is directed ; ::_thesis: Net-Str (S,f) in NetUniv R
reconsider N = Net-Str (S,f) as strict net of R by A2;
set UN = the_universe_of the carrier of R;
reconsider UN = the_universe_of the carrier of R as universal set ;
 the_transitive-closure_of the carrier of R in UN by CLASSES1:2;
then  the carrier of R in UN by CLASSES1:3, CLASSES1:52;
then A3: S in UN by A1, CLASSES1:def_1;
 the carrier of N = S by Def10;
hence  Net-Str (S,f) in NetUniv R by A3, YELLOW_6:def_11; ::_thesis: verum
end;

registration
let R be LATTICE;
cluster non empty reflexive transitive strict directed monotone for NetStr over R;
existence
 ex b1 being net of R st
( b1 is monotone & b1 is reflexive & b1 is strict )
proof
reconsider f = id the carrier of R as Function of the carrier of R, the carrier of R ;
 rng f = [#] R by RELAT_1:45;
then reconsider N = Net-Str ( the carrier of R,f) as reflexive strict net of R by Th20;
take  N ; ::_thesis: ( N is monotone & N is reflexive & N is strict )
thus  ( N is monotone & N is reflexive & N is strict ) ; ::_thesis: verum
end;
end;

theorem Th22: :: WAYBEL11:22
for R being complete LATTICE
for N being reflexive monotone net of R holds lim_inf N = sup N
proof
let R be complete LATTICE; ::_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
defpred S1[ set ] 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]  }  ;
deffunc H2( Element of N) ->  Element of the carrier of R = N . $1;
A1: for j being Element of N holds H2(j) = H1(j)
proof
let j be Element of N; ::_thesis: H2(j) = H1(j)
set Y =  {  (N . i) where i is Element of N : i >= j  }  ;
A2: N . j is_<=_than  {  (N . i) where i is Element of N : i >= j  }
proof
let y be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not y in  {  (N . i) where i is Element of N : i >= j  }  or N . j <= y )
assume  y in  {  (N . i) where i is Element of N : i >= j  }  ; ::_thesis: N . j <= y
then  ex i being Element of N st
( y = N . i & j <= i ) ;
hence  N . j <= y by Def9; ::_thesis: verum
end;
 for b being Element of R st b is_<=_than  {  (N . i) where i is Element of N : i >= j  }  holds
N . j >= b
proof
let b be Element of R; ::_thesis: ( b is_<=_than  {  (N . i) where i is Element of N : i >= j  }  implies N . j >= b )
assume A3: b is_<=_than  {  (N . i) where i is Element of N : i >= j  }  ; ::_thesis: N . j >= b
reconsider j9 = j as Element of N ;
 j9 <= j9 ;
then  N . j9 in  {  (N . i) where i is Element of N : i >= j  }  ;
hence  N . j >= b by A3, LATTICE3:def_8; ::_thesis: verum
end;
hence  H2(j) = H1(j) by A2, YELLOW_0:33; ::_thesis: verum
end;
rng the mapping of N =  {  H2(j) where j is Element of N : S1[j]  }  by Th19
.=  {  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 Th23: :: WAYBEL11:23
for R being complete LATTICE
for N being constant net of R holds the_value_of N = lim_inf N
proof
let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N = lim_inf N
let N be constant net of R; ::_thesis: the_value_of N = lim_inf N
set X =  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ;
set j = the Element of N;
A1: N . the Element of N is_>=_than  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }
proof
let b be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not b in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  or b <= N . the Element of N )
assume  b in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ; ::_thesis: b <= N . the Element of N
then consider j0 being Element of N such that
A2: b = "/\" ( {  (N . i) where i is Element of N : i >= j0  }  ,R) ;
reconsider j0 = j0 as Element of N ;
consider i0 being Element of N such that
A3: i0 >= j0 and
 i0 >= j0 by YELLOW_6:def_3;
A4: N . i0 in  {  (N . i) where i is Element of N : i >= j0  }  by A3;
N . i0 = the_value_of N by YELLOW_6:16
.= N . the Element of N by YELLOW_6:16 ;
hence  b <= N . the Element of N by A2, A4, YELLOW_2:22; ::_thesis: verum
end;
A5: for b being Element of R st b is_>=_than  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  holds
N . the Element of N <= b
proof
let b be Element of R; ::_thesis: ( b is_>=_than  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  implies N . the Element of N <= b )
set Y =  {  (N . i) where i is Element of N : i >= the Element of N  }  ;
A6: "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,R) in  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ;
assume  b is_>=_than  {  ("/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R)) where j is Element of N : verum  }  ; ::_thesis: N . the Element of N <= b
then A7: b >= "/\" ( {  (N . i) where i is Element of N : i >= the Element of N  }  ,R) by A6, LATTICE3:def_9;
A8: N . the Element of N is_<=_than  {  (N . i) where i is Element of N : i >= the Element of N  }
proof
let c be Element of R; :: according to LATTICE3:def_8 ::_thesis: ( not c in  {  (N . i) where i is Element of N : i >= the Element of N  }  or N . the Element of N <= c )
assume  c in  {  (N . i) where i is Element of N : i >= the Element of N  }  ; ::_thesis: N . the Element of N <= c
then consider i0 being Element of N such that
A9: c = N . i0 and
 i0 >= the Element of N ;
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence  N . the Element of N <= c by A9; ::_thesis: verum
end;
 for b being Element of R st b is_<=_than  {  (N . i) where i is Element of N : i >= the Element of N  }  holds
N . the Element of N >= b
proof
let c be Element of R; ::_thesis: ( c is_<=_than  {  (N . i) where i is Element of N : i >= the Element of N  }  implies N . the Element of N >= c )
consider i0 being Element of N such that
A10: i0 >= the Element of N and
 i0 >= the Element of N by YELLOW_6:def_3;
A11: N . i0 in  {  (N . i) where i is Element of N : i >= the Element of N  }  by A10;
assume A12: c is_<=_than  {  (N . i) where i is Element of N : i >= the Element of N  }  ; ::_thesis: N . the Element of N >= c
N . the Element of N = the_value_of N by YELLOW_6:16
.= N . i0 by YELLOW_6:16 ;
hence  N . the Element of N >= c by A11, A12, LATTICE3:def_8; ::_thesis: verum
end;
hence  N . the Element of N <= b by A7, A8, YELLOW_0:33; ::_thesis: verum
end;
thus  the_value_of N = N . the Element of N by YELLOW_6:16
.= lim_inf N by A1, A5, YELLOW_0:32 ; ::_thesis: verum
end;

theorem Th24: :: WAYBEL11:24
for R being complete LATTICE
for N being constant net of R holds the_value_of N is_S-limit_of N
proof
let R be complete LATTICE; ::_thesis: for N being constant net of R holds the_value_of N is_S-limit_of N
let N be constant net of R; ::_thesis: the_value_of N is_S-limit_of N
 the_value_of N <= lim_inf N by Th23;
hence  the_value_of N is_S-limit_of N by Def7; ::_thesis: verum
end;

definition
let S be non empty 1-sorted ;
let e be Element of S;
func Net-Str e ->  strict NetStr over S means :Def11: :: WAYBEL11:def 11
( the carrier of it = {e} & the InternalRel of it = {[e,e]} & the mapping of it = id {e} );
existence
 ex b1 being strict NetStr over S st
( the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} )
proof
 e in {e} by TARSKI:def_1;
then reconsider r = {[e,e]} as Relation of {e} by RELSET_1:3;
A1: dom (id {e}) = {e} by RELAT_1:45;
 rng (id {e}) = {e} by RELAT_1:45;
then reconsider f = id {e} as Function of {e}, the carrier of S by A1, RELSET_1:4;
take  NetStr(# {e},r,f #) ; ::_thesis: ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} )
thus  ( the carrier of NetStr(# {e},r,f #) = {e} & the InternalRel of NetStr(# {e},r,f #) = {[e,e]} & the mapping of NetStr(# {e},r,f #) = id {e} ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict NetStr over S st the carrier of b1 = {e} & the InternalRel of b1 = {[e,e]} & the mapping of b1 = id {e} & the carrier of b2 = {e} & the InternalRel of b2 = {[e,e]} & the mapping of b2 = id {e} holds
b1 = b2 ;
end;

:: deftheorem Def11 defines Net-Str WAYBEL11:def_11_:_
 for S being non empty 1-sorted
for e being Element of S
for b3 being strict NetStr over S holds
( b3 = Net-Str e iff ( the carrier of b3 = {e} & the InternalRel of b3 = {[e,e]} & the mapping of b3 = id {e} ) );

registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e ->  non empty strict ;
coherence
 not Net-Str e is empty
proof
set N = Net-Str e;
 the carrier of (Net-Str e) = {e} by Def11;
hence  not the carrier of (Net-Str e) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem Th25: :: WAYBEL11:25
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds x = e
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for x being Element of (Net-Str e) holds x = e
let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds x = e
let x be Element of (Net-Str e); ::_thesis: x = e
 the carrier of (Net-Str e) = {e} by Def11;
hence  x = e by TARSKI:def_1; ::_thesis: verum
end;

theorem Th26: :: WAYBEL11:26
for S being non empty 1-sorted
for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let e be Element of S; ::_thesis: for x being Element of (Net-Str e) holds (Net-Str e) . x = e
let x be Element of (Net-Str e); ::_thesis: (Net-Str e) . x = e
set N = Net-Str e;
A1: the carrier of (Net-Str e) = {e} by Def11;
then A2: x = e by TARSKI:def_1;
thus (Net-Str e) . x = (id {e}) . x by Def11
.= e by A1, A2, FUNCT_1:18 ; ::_thesis: verum
end;

registration
let S be non empty 1-sorted ;
let e be Element of S;
cluster Net-Str e ->  reflexive transitive antisymmetric strict directed ;
coherence
 ( Net-Str e is reflexive & Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )
proof
set N = Net-Str e;
 the carrier of (Net-Str e) = {e} by Def11;
then reconsider e = e as Element of (Net-Str e) by TARSKI:def_1;
 the InternalRel of (Net-Str e) = {[e,e]} by Def11;
then A1: [e,e] in the InternalRel of (Net-Str e) by TARSKI:def_1;
thus  Net-Str e is reflexive ::_thesis: ( Net-Str e is transitive & Net-Str e is directed & Net-Str e is antisymmetric )
proof
let x be Element of (Net-Str e); :: according to YELLOW_0:def_1 ::_thesis: x <= x
 x = e by Th25;
hence  x <= x by A1, ORDERS_2:def_5; ::_thesis: verum
end;
thus  Net-Str e is transitive ::_thesis: ( Net-Str e is directed & Net-Str e is antisymmetric )
proof
let x, y, z be Element of (Net-Str e); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
 x <= y and
 y <= z ; ::_thesis: x <= z
A2: x = e by Th25;
 z = e by Th25;
hence  x <= z by A1, A2, ORDERS_2:def_5; ::_thesis: verum
end;
thus  Net-Str e is directed ::_thesis: Net-Str e is antisymmetric
proof
let x, y be Element of (Net-Str e); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of (Net-Str e) st
( x <= b1 & y <= b1 )
take  e ; ::_thesis: ( x <= e & y <= e )
A3: x = e by Th25;
 y = e by Th25;
hence  ( x <= e & y <= e ) by A1, A3, ORDERS_2:def_5; ::_thesis: verum
end;
let x, y be Element of (Net-Str e); :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
assume that
 x <= y and
 y <= x ; ::_thesis: x = y
 x = e by Th25;
hence  x = y by Th25; ::_thesis: verum
end;
end;

theorem Th27: :: WAYBEL11:27
for S being non empty 1-sorted
for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
proof
let S be non empty 1-sorted ; ::_thesis: for e being Element of S
for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let e be Element of S; ::_thesis: for X being set holds
( Net-Str e is_eventually_in X iff e in X )
let X be set ; ::_thesis: ( Net-Str e is_eventually_in X iff e in X )
set N = Net-Str e;
 the carrier of (Net-Str e) = {e} by Def11;
then reconsider d = e as Element of (Net-Str e) by TARSKI:def_1;
hereby  ::_thesis: ( e in X implies Net-Str e is_eventually_in X )
assume  Net-Str e is_eventually_in X ; ::_thesis: e in X
then consider x being Element of (Net-Str e) such that
A1: for y being Element of (Net-Str e) st x <= y holds
(Net-Str e) . y in X by WAYBEL_0:def_11;
 (Net-Str e) . x in X by A1;
hence  e in X by Th26; ::_thesis: verum
end;
assume A2: e in X ; ::_thesis: Net-Str e is_eventually_in X
take  d ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (Net-Str e) holds
( not d <= b1 or (Net-Str e) . b1 in X )
let j be Element of (Net-Str e); ::_thesis: ( not d <= j or (Net-Str e) . j in X )
assume  d <= j ; ::_thesis: (Net-Str e) . j in X
thus  (Net-Str e) . j in X by A2, Th26; ::_thesis: verum
end;

theorem Th28: :: WAYBEL11:28
for S being non empty reflexive antisymmetric RelStr
for e being Element of S holds e = lim_inf (Net-Str e)
proof
let S be non empty reflexive antisymmetric RelStr ; ::_thesis: for e being Element of S holds e = lim_inf (Net-Str e)
let e be Element of S; ::_thesis: e = lim_inf (Net-Str e)
set N = Net-Str e;
set X =  {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  ;
reconsider e9 = e as Element of S ;
A1:  {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  c= {e9}
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  or u in {e9} )
assume  u in  {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  ; ::_thesis: u in {e9}
then consider j being Element of (Net-Str e) such that
A2: u = "/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S) ;
set Y =  {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ;
A3:  {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  c= {e9}
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in  {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  or v in {e9} )
assume  v in  {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ; ::_thesis: v in {e9}
then consider i being Element of (Net-Str e) such that
A4: v = (Net-Str e) . i and
 i >= j ;
reconsider i9 = i as Element of (Net-Str e) ;
 (Net-Str e) . i9 = e by Th26;
hence  v in {e9} by A4, TARSKI:def_1; ::_thesis: verum
end;
reconsider j9 = j as Element of (Net-Str e) ;
 j9 <= j9 ;
then  (Net-Str e) . j in  {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ;
then   {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  = {e9} by A3, ZFMISC_1:33;
then  u = e9 by A2, YELLOW_0:39;
hence  u in {e9} by TARSKI:def_1; ::_thesis: verum
end;
set j = the Element of (Net-Str e);
 "/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= the Element of (Net-Str e)  }  ,S) in  {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  ;
then   {  ("/\" ( {  ((Net-Str e) . i) where i is Element of (Net-Str e) : i >= j  }  ,S)) where j is Element of (Net-Str e) : verum  }  = {e9} by A1, ZFMISC_1:33;
hence  e = lim_inf (Net-Str e) by YELLOW_0:39; ::_thesis: verum
end;

theorem Th29: :: WAYBEL11:29
for S being non empty reflexive RelStr
for e being Element of S holds Net-Str e in NetUniv S
proof
let S be non empty reflexive RelStr ; ::_thesis: for e being Element of S holds Net-Str e in NetUniv S
let e be Element of S; ::_thesis: Net-Str e in NetUniv S
set N = Net-Str e;
set UN = the_universe_of the carrier of S;
A1: the carrier of (Net-Str e) = {e} by Def11;
reconsider UN = the_universe_of the carrier of S as universal set ;
 the_transitive-closure_of the carrier of S in UN by CLASSES1:2;
then  the carrier of S in UN by CLASSES1:3, CLASSES1:52;
then  the carrier of (Net-Str e) in the_universe_of the carrier of S by A1, CLASSES1:def_1;
hence  Net-Str e in NetUniv S by YELLOW_6:def_11; ::_thesis: verum
end;

theorem Th30: :: WAYBEL11:30
for R being complete LATTICE
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 LATTICE; ::_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;
set E1 =  {  (Z . k) where k is Element of Z : k >= jx  }  ;
set Ey =  {  (Z . k) where k is Element of Z : k >= jy  }  ;
set E =  {  (Z . k) where k is Element of Z : k >= j  }  ;
take z = "/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R); ::_thesis: ( z in D & x <= z & y <= z )
thus  z in D by A1; ::_thesis: ( x <= z & y <= z )
  {  (Z . k) where k is Element of Z : k >= j  }  c=  {  (Z . k) where k is Element of Z : k >= jx  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (Z . k) where k is Element of Z : k >= j  }  or e in  {  (Z . k) where k is Element of Z : k >= jx  }  )
assume  e in  {  (Z . k) where k is Element of Z : k >= j  }  ; ::_thesis: e in  {  (Z . k) where k is Element of Z : k >= jx  }
then consider k being Element of Z such that
A6: e = Z . k and
A7: k >= j ;
reconsider k = k as Element of Z ;
 k >= jx by A4, A7, YELLOW_0:def_2;
hence  e in  {  (Z . k) where k is Element of Z : k >= jx  }  by A6; ::_thesis: verum
end;
hence  x <= z by A2, WAYBEL_7:1; ::_thesis: y <= z
  {  (Z . k) where k is Element of Z : k >= j  }  c=  {  (Z . k) where k is Element of Z : k >= jy  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (Z . k) where k is Element of Z : k >= j  }  or e in  {  (Z . k) where k is Element of Z : k >= jy  }  )
assume  e in  {  (Z . k) where k is Element of Z : k >= j  }  ; ::_thesis: e in  {  (Z . k) where k is Element of Z : k >= jy  }
then consider k being Element of Z such that
A8: e = Z . k and
A9: k >= j ;
reconsider k = k as Element of Z ;
 k >= jy by A5, A9, YELLOW_0:def_2;
hence  e in  {  (Z . k) where k is Element of Z : k >= jy  }  by A8; ::_thesis: verum
end;
hence  y <= z by A3, WAYBEL_7:1; ::_thesis: verum
end;

theorem Th31: :: WAYBEL11:31
for L being complete LATTICE
for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
proof
let L be complete LATTICE; ::_thesis: for S being Subset of L holds
( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
set SC = Scott-Convergence L;
set T = ConvergenceSpace (Scott-Convergence L);
A1: the topology of (ConvergenceSpace (Scott-Convergence L)) =  {  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 Scott-Convergence L holds
N is_eventually_in V  }  by YELLOW_6:def_24;
let S be Subset of L; ::_thesis: ( S in the topology of (ConvergenceSpace (Scott-Convergence L)) iff ( S is inaccessible & S is upper ) )
hereby  ::_thesis: ( S is inaccessible & S is upper implies S in the topology of (ConvergenceSpace (Scott-Convergence L)) )
assume  S in the topology of (ConvergenceSpace (Scott-Convergence L)) ; ::_thesis: ( S is inaccessible & S is upper )
then A2: ex V being Subset of L st
( S = V & ( for p being Element of L st p in V holds
for N being net of L st [N,p] in Scott-Convergence L 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 L; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume A3: sup D in S ; ::_thesis: D meets 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 L by A4, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of L by A5, Th20;
A6: N in NetUniv L by Th21;
lim_inf N = sup N by Th22
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),L) by YELLOW_2:def_5
.= "\/" ((rng f),L) by Def10
.= sup D by RELAT_1:45 ;
then  sup D is_S-limit_of N by Def7;
then  [N,(sup D)] in Scott-Convergence L by A6, Def8;
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 Def10;
N . j0 = (id D) . j0 by Def10
.= j0 by A10, FUNCT_1:18 ;
hence  D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus  S is upper ::_thesis: verum
proof
let x, y be Element of L; :: 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 L by Th29;
 y = lim_inf (Net-Str y) by Th28;
then  x is_S-limit_of Net-Str y by A12, Def7;
then  [(Net-Str y),x] in Scott-Convergence L by A13, Def8;
then  Net-Str y is_eventually_in S by A2, A11;
hence  y in S by Th27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S in the topology of (ConvergenceSpace (Scott-Convergence L))
 for p being Element of L st p in S holds
for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
proof
let p be Element of L; ::_thesis: ( p in S implies for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of L st [N,p] in Scott-Convergence L holds
N is_eventually_in S
reconsider p9 = p as Element of L ;
let N be net of L; ::_thesis: ( [N,p] in Scott-Convergence L implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence L ; ::_thesis: N is_eventually_in S
 Scott-Convergence L c= [:(NetUniv L), the carrier of L:] by YELLOW_6:def_18;
then A18: N in NetUniv L by A17, ZFMISC_1:87;
then  ex N9 being strict net of L st
( N9 = N & the carrier of N9 in the_universe_of the carrier of L ) by YELLOW_6:def_11;
then  p is_S-limit_of N by A17, A18, Def8;
then A19: p9 <= lim_inf N by Def7;
defpred S1[ set ] means verum;
deffunc H1( Element of N) ->  Element of the carrier of L = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,L);
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 L from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of L ;
reconsider D = D as non empty directed Subset of L by Th30;
 sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then  D meets S by A14, Def1;
then  D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of L such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of L ;
 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  }  ,L) ;
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  {  (N . i) where i is Element of N : i >= j  }  ;
then  d <= N . i0 by A21, YELLOW_2:22;
hence  N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
hence  S in the topology of (ConvergenceSpace (Scott-Convergence L)) by A1; ::_thesis: verum
end;

theorem Th32: :: WAYBEL11:32
for T being complete Scott TopLattice holds TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
proof
let T be complete Scott TopLattice; ::_thesis: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T)
set CSC = ConvergenceSpace (Scott-Convergence T);
 the topology of T = the topology of (ConvergenceSpace (Scott-Convergence T))
proof
thus  the topology of T c= the topology of (ConvergenceSpace (Scott-Convergence T)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence T)) c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of T or e in the topology of (ConvergenceSpace (Scott-Convergence T)) )
assume A1: e in the topology of T ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence T))
then reconsider A = e as Subset of T ;
 A is open by A1, PRE_TOPC:def_2;
then  ( A is inaccessible & A is upper ) by Def4;
hence  e in the topology of (ConvergenceSpace (Scott-Convergence T)) by Th31; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence T)) or e in the topology of T )
assume A2: e in the topology of (ConvergenceSpace (Scott-Convergence T)) ; ::_thesis: e in the topology of T
then reconsider A = e as Subset of T by YELLOW_6:def_24;
 ( A is inaccessible & A is upper ) by A2, Th31;
then  A is open by Def4;
hence  e in the topology of T by PRE_TOPC:def_2; ::_thesis: verum
end;
hence  TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by YELLOW_6:def_24; ::_thesis: verum
end;

theorem Th33: :: WAYBEL11:33
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )
proof
let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) )
set SC = Scott-Convergence T;
assume  TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) )
then A1: the topology of T =  {  V where V is Subset of T : for p being Element of T st p in V holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in V  }  by YELLOW_6:def_24;
let S be Subset of T; ::_thesis: ( S is open iff ( S is inaccessible & S is upper ) )
hereby  ::_thesis: ( S is inaccessible & S is upper implies S is open )
assume  S is open ; ::_thesis: ( S is inaccessible & S is upper )
then  S in the topology of T by PRE_TOPC:def_2;
then A2: ex V being Subset of T st
( S = V & ( for p being Element of T st p in V holds
for N being net of T st [N,p] in Scott-Convergence T 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 T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume A3: sup D in S ; ::_thesis: D meets 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 T by A4, RELSET_1:4;
reconsider N = Net-Str (D,f) as reflexive strict monotone net of T by A5, Th20;
A6: N in NetUniv T by Th21;
lim_inf N = sup N by Th22
.= Sup by WAYBEL_2:def_1
.= "\/" ((rng the mapping of N),T) by YELLOW_2:def_5
.= "\/" ((rng f),T) by Def10
.= sup D by RELAT_1:45 ;
then  sup D is_S-limit_of N by Def7;
then  [N,(sup D)] in Scott-Convergence T by A6, Def8;
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 Def10;
N . j0 = (id D) . j0 by Def10
.= j0 by A10, FUNCT_1:18 ;
hence  D meets S by A9, A10, XBOOLE_0:3; ::_thesis: verum
end;
thus  S is upper ::_thesis: verum
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
A11: x in S and
A12: x <= y ; ::_thesis: y in S
A13: Net-Str y in NetUniv T by Th29;
 y = lim_inf (Net-Str y) by Th28;
then  x is_S-limit_of Net-Str y by A12, Def7;
then  [(Net-Str y),x] in Scott-Convergence T by A13, Def8;
then  Net-Str y is_eventually_in S by A2, A11;
hence  y in S by Th27; ::_thesis: verum
end;
end;
assume that
A14: S is inaccessible and
A15: S is upper ; ::_thesis: S is open
 for p being Element of T st p in S holds
for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
proof
let p be Element of T; ::_thesis: ( p in S implies for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S )
assume A16: p in S ; ::_thesis: for N being net of T st [N,p] in Scott-Convergence T holds
N is_eventually_in S
reconsider p9 = p as Element of T ;
let N be net of T; ::_thesis: ( [N,p] in Scott-Convergence T implies N is_eventually_in S )
assume A17: [N,p] in Scott-Convergence T ; ::_thesis: N is_eventually_in S
 Scott-Convergence T c= [:(NetUniv T), the carrier of T:] by YELLOW_6:def_18;
then A18: N in NetUniv T by A17, ZFMISC_1:87;
then  ex N9 being strict net of T st
( N9 = N & the carrier of N9 in the_universe_of the carrier of T ) by YELLOW_6:def_11;
then  p is_S-limit_of N by A17, A18, Def8;
then A19: p9 <= lim_inf N by Def7;
defpred S1[ set ] means verum;
deffunc H1( Element of N) ->  Element of the carrier of T = "/\" ( {  (N . i) where i is Element of N : i >= $1  }  ,T);
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 T from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of T ;
reconsider D = D as non empty directed Subset of T by Th30;
 sup D in S by A15, A16, A19, WAYBEL_0:def_20;
then  D meets S by A14, Def1;
then  D /\ S <> {} by XBOOLE_0:def_7;
then consider d being Element of T such that
A20: d in D /\ S by SUBSET_1:4;
reconsider d = d as Element of T ;
 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  }  ,T) ;
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  {  (N . i) where i is Element of N : i >= j  }  ;
then  d <= N . i0 by A21, YELLOW_2:22;
hence  N . i0 in S by A15, A22, WAYBEL_0:def_20; ::_thesis: verum
end;
then  S in the topology of T by A1;
hence  S is open by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem Th34: :: WAYBEL11:34
for T being complete TopLattice st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) holds
T is Scott
proof
let T be complete TopLattice; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) implies T is Scott )
assume  TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) ; ::_thesis: T is Scott
hence  for S being Subset of T holds
( S is open iff ( S is inaccessible & S is upper ) ) by Th33; :: according to WAYBEL11:def_4 ::_thesis: verum
end;

registration
let R be complete LATTICE;
cluster Scott-Convergence R ->  (CONSTANTS) ;
coherence
 Scott-Convergence R is (CONSTANTS)
proof
let N be constant net of R; :: according to YELLOW_6:def_20 ::_thesis: ( not N in NetUniv R or [N,(the_value_of N)] in Scott-Convergence R )
assume A1: N in NetUniv R ; ::_thesis: [N,(the_value_of N)] in Scott-Convergence R
then consider M being strict net of R such that
A2: M = N and
 the carrier of M in the_universe_of the carrier of R by YELLOW_6:def_11;
 the_value_of M is_S-limit_of M by A2, Th24;
hence  [N,(the_value_of N)] in Scott-Convergence R by A1, A2, Def8; ::_thesis: verum
end;
end;

registration
let R be complete LATTICE;
cluster Scott-Convergence R ->  (SUBNETS) ;
coherence
 Scott-Convergence R is (SUBNETS)
proof
set S = Scott-Convergence R;
let N be net of R; :: according to YELLOW_6:def_21 ::_thesis: for b1 being subnet of N holds
( not b1 in NetUniv R or for b2 being Element of the carrier of R holds
( not [N,b2] in Scott-Convergence R or [b1,b2] in Scott-Convergence R ) )
let Y be subnet of N; ::_thesis: ( not Y in NetUniv R or for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R ) )
A1: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
assume A2: Y in NetUniv R ; ::_thesis: for b1 being Element of the carrier of R holds
( not [N,b1] in Scott-Convergence R or [Y,b1] in Scott-Convergence R )
then consider Y9 being strict net of R such that
A3: Y9 = Y and
 the carrier of Y9 in the_universe_of the carrier of R by YELLOW_6:def_11;
let p be Element of R; ::_thesis: ( not [N,p] in Scott-Convergence R or [Y,p] in Scott-Convergence R )
assume A4: [N,p] in Scott-Convergence R ; ::_thesis: [Y,p] in Scott-Convergence R
then A5: N in NetUniv R by A1, ZFMISC_1:87;
then consider N9 being strict net of R such that
A6: N9 = N and
 the carrier of N9 in the_universe_of the carrier of R by YELLOW_6:def_11;
deffunc H1( Element of N) ->  Element of the carrier of R = "/\" ( {  (N . i) where i is Element of N : i >= R  }  ,R);
defpred S1[ set ] means verum;
reconsider X1 =  {  H1(j) where j is Element of N : S1[j]  }  as Subset of R from DOMAIN_1:sch_8();
deffunc H2( Element of Y) ->  Element of the carrier of R = "/\" ( {  (Y . i) where i is Element of Y : i >= R  }  ,R);
reconsider X2 =  {  H2(j) where j is Element of Y : S1[j]  }  as Subset of R from DOMAIN_1:sch_8();
 p is_S-limit_of N9 by A4, A5, A6, Def8;
then A7: p <= lim_inf N by A6, Def7;
consider f being Function of Y,N such that
A8: the mapping of Y = the mapping of N * f and
A9: for m being Element of N ex n being Element of Y st
for p being Element of Y st n <= p holds
m <= f . p by YELLOW_6:def_9;
 X1 is_finer_than X2
proof
let a be Element of R; :: according to YELLOW_4:def_1 ::_thesis: ( not a in X1 or ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 ) )
assume  a in X1 ; ::_thesis: ex b1 being Element of the carrier of R st
( b1 in X2 & a <= b1 )
then consider j being Element of N such that
A10: a = "/\" ( {  (N . i) where i is Element of N : i >= j  }  ,R) ;
reconsider j = j as Element of N ;
consider n being Element of Y such that
A11: for p being Element of Y st n <= p holds
j <= f . p by A9;
set X3 =  {  (Y . i) where i is Element of Y : i >= n  }  ;
set X4 =  {  (N . i) where i is Element of N : i >= j  }  ;
take b = "/\" ( {  (Y . i) where i is Element of Y : i >= n  }  ,R); ::_thesis: ( b in X2 & a <= b )
thus  b in X2 ; ::_thesis: a <= b
  {  (Y . i) where i is Element of Y : i >= n  }  c=  {  (N . i) where i is Element of N : i >= j  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (Y . i) where i is Element of Y : i >= n  }  or u in  {  (N . i) where i is Element of N : i >= j  }  )
assume  u in  {  (Y . i) where i is Element of Y : i >= n  }  ; ::_thesis: u in  {  (N . i) where i is Element of N : i >= j  }
then consider m being Element of Y such that
A12: u = Y . m and
A13: m >= n ;
reconsider m = m as Element of Y ;
A14: f . m >= j by A11, A13;
 u = N . (f . m) by A8, A12, FUNCT_2:15;
hence  u in  {  (N . i) where i is Element of N : i >= j  }  by A14; ::_thesis: verum
end;
hence  a <= b by A10, WAYBEL_7:1; ::_thesis: verum
end;
then  "\/" (X1,R) <= "\/" (X2,R) by Th2;
then  p <= lim_inf Y by A7, YELLOW_0:def_2;
then  p is_S-limit_of Y9 by A3, Def7;
hence  [Y,p] in Scott-Convergence R by A2, A3, Def8; ::_thesis: verum
end;
end;

theorem Th35: :: WAYBEL11:35
for S being non empty 1-sorted
for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
proof
let S be non empty 1-sorted ; ::_thesis: for N being net of S
for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let N be net of S; ::_thesis: for X being set
for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let X be set ; ::_thesis: for M being subnet of N st M = N " X holds
for i being Element of M holds M . i in X
let M be subnet of N; ::_thesis: ( M = N " X implies for i being Element of M holds M . i in X )
assume A1: M = N " X ; ::_thesis: for i being Element of M holds M . i in X
let j be Element of M; ::_thesis: M . j in X
 j in the carrier of M ;
then  j in the mapping of N " X by A1, YELLOW_6:def_10;
then A2: the mapping of N . j in X by FUNCT_1:def_7;
 the mapping of M = the mapping of N | the carrier of M by A1, YELLOW_6:def_6;
hence  M . j in X by A2, FUNCT_1:49; ::_thesis: verum
end;

definition
let L be non empty reflexive RelStr ;
func sigma L ->  Subset-Family of L equals :: WAYBEL11:def 12
 the topology of (ConvergenceSpace (Scott-Convergence L));
coherence
 the topology of (ConvergenceSpace (Scott-Convergence L)) is Subset-Family of L by YELLOW_6:def_24;
end;

:: deftheorem  defines sigma WAYBEL11:def_12_:_
 for L being non empty reflexive RelStr holds sigma L = the topology of (ConvergenceSpace (Scott-Convergence L));

theorem Th36: :: WAYBEL11:36
for L being complete continuous Scott TopLattice
for x being Element of L holds wayabove x is open
proof
let L be complete continuous Scott TopLattice; ::_thesis: for x being Element of L holds wayabove x is open
let x be Element of L; ::_thesis: wayabove x is open
set W = wayabove x;
 wayabove x is inaccessible
proof
let D be non empty directed Subset of L; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in wayabove x implies D meets wayabove x )
assume  sup D in wayabove x ; ::_thesis: D meets wayabove x
then  x << sup D by WAYBEL_3:8;
then consider d being Element of L such that
A1: d in D and
A2: x << d by WAYBEL_4:53;
 d in wayabove x by A2;
hence  D meets wayabove x by A1, XBOOLE_0:3; ::_thesis: verum
end;
hence  wayabove x is open by Def4; ::_thesis: verum
end;

theorem Th37: :: WAYBEL11:37
for T being complete TopLattice st the topology of T = sigma T holds
T is Scott
proof
let T be complete TopLattice; ::_thesis: ( the topology of T = sigma T implies T is Scott )
set CSC = ConvergenceSpace (Scott-Convergence T);
assume  the topology of T = sigma T ; ::_thesis: T is Scott
then  TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of (ConvergenceSpace (Scott-Convergence T)), the topology of (ConvergenceSpace (Scott-Convergence T)) #) by YELLOW_6:def_24;
hence  T is Scott by Th34; ::_thesis: verum
end;

Lm3:  for T1, T2 being TopStruct st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like holds
T2 is TopSpace-like
proof
let T1, T2 be TopStruct ; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) & T1 is TopSpace-like implies T2 is TopSpace-like )
assume that
A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) and
A2: T1 is TopSpace-like ; ::_thesis: T2 is TopSpace-like
thus  the carrier of T2 in the topology of T2 by A1, A2, PRE_TOPC:def_1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of T2) holds
( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds
( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) )
thus  ( ( for b1 being Element of bool (bool the carrier of T2) holds
( not b1 c= the topology of T2 or union b1 in the topology of T2 ) ) & ( for b1, b2 being Element of bool the carrier of T2 holds
( not b1 in the topology of T2 or not b2 in the topology of T2 or b1 /\ b2 in the topology of T2 ) ) ) by A1, A2, PRE_TOPC:def_1; ::_thesis: verum
end;

Lm4:  for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
for N being strict net of S1 holds N is strict net of S2
;

Lm5:  for S1, S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 holds
NetUniv S1 = NetUniv S2
proof
let S1, S2 be non empty 1-sorted ; ::_thesis: ( the carrier of S1 = the carrier of S2 implies NetUniv S1 = NetUniv S2 )
assume A1: the carrier of S1 = the carrier of S2 ; ::_thesis: NetUniv S1 = NetUniv S2
defpred S1[ set ] means  ex N being strict net of S2 st
( N = $1 & the carrier of N in the_universe_of the carrier of S2 );
A2: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_NetUniv_S1_implies_S1[x]_)_&_(_S1[x]_implies_x_in_NetUniv_S1_)_)
let x be set ; ::_thesis: ( ( x in NetUniv S1 implies S1[x] ) & ( S1[x] implies x in NetUniv S1 ) )
hereby  ::_thesis: ( S1[x] implies x in NetUniv S1 )
assume  x in NetUniv S1 ; ::_thesis: S1[x]
then consider N being strict net of S1 such that
A3: N = x and
A4: the carrier of N in the_universe_of the carrier of S1 by YELLOW_6:def_11;
reconsider N = N as strict net of S2 by A1;
thus  S1[x] ::_thesis: verum
proof
take  N ; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S2 )
thus  ( N = x & the carrier of N in the_universe_of the carrier of S2 ) by A1, A3, A4; ::_thesis: verum
end;
end;
assume  S1[x] ; ::_thesis: x in NetUniv S1
then consider N being strict net of S2 such that
A5: N = x and
A6: the carrier of N in the_universe_of the carrier of S2 ;
reconsider N = N as strict net of S1 by A1;
now__::_thesis:_ex_N_being_strict_net_of_S1_st_
(_N_=_x_&_the_carrier_of_N_in_the_universe_of_the_carrier_of_S1_)
take N = N; ::_thesis: ( N = x & the carrier of N in the_universe_of the carrier of S1 )
thus  ( N = x & the carrier of N in the_universe_of the carrier of S1 ) by A1, A5, A6; ::_thesis: verum
end;
hence  x in NetUniv S1 by YELLOW_6:def_11; ::_thesis: verum
end;
A7: for x being set holds
( x in NetUniv S2 iff S1[x] ) by YELLOW_6:def_11;
thus  NetUniv S1 = NetUniv S2 from XBOOLE_0:sch_2(A2, A7); ::_thesis: verum
end;

Lm6:  for T1, T2 being non empty 1-sorted
for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
proof
let T1, T2 be non empty 1-sorted ; ::_thesis: for X being set
for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let X be set ; ::_thesis: for N1 being net of T1
for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 & N1 is_eventually_in X holds
N2 is_eventually_in X
let N2 be net of T2; ::_thesis: ( N1 = N2 & N1 is_eventually_in X implies N2 is_eventually_in X )
assume A1: N1 = N2 ; ::_thesis: ( not N1 is_eventually_in X or N2 is_eventually_in X )
assume  N1 is_eventually_in X ; ::_thesis: N2 is_eventually_in X
then consider i being Element of N1 such that
A2: for j being Element of N1 st i <= j holds
N1 . j in X by WAYBEL_0:def_11;
reconsider ii = i as Element of N2 by A1;
take  ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds
( not ii <= b1 or N2 . b1 in X )
let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in X )
reconsider j = jj as Element of N1 by A1;
assume A3: ii <= jj ; ::_thesis: N2 . jj in X
 N2 . jj = N1 . j by A1;
hence  N2 . jj in X by A1, A2, A3; ::_thesis: verum
end;

Lm7:  for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2 )
assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: for N1 being net of T1
for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let N1 be net of T1; ::_thesis: for N2 being net of T2 st N1 = N2 holds
for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let N2 be net of T2; ::_thesis: ( N1 = N2 implies for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2 )
assume A2: N1 = N2 ; ::_thesis: for p1 being Point of T1
for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let p1 be Point of T1; ::_thesis: for p2 being Point of T2 st p1 = p2 & p1 in Lim N1 holds
p2 in Lim N2
let p2 be Point of T2; ::_thesis: ( p1 = p2 & p1 in Lim N1 implies p2 in Lim N2 )
assume that
A3: p1 = p2 and
A4: p1 in Lim N1 ; ::_thesis: p2 in Lim N2
 for V being a_neighborhood of p2 holds N2 is_eventually_in V
proof
let V be a_neighborhood of p2; ::_thesis: N2 is_eventually_in V
reconsider W = V as Subset of T1 by A1;
 p2 in Int V by CONNSP_2:def_1;
then consider G being Subset of T2 such that
A5: G is open and
A6: G c= V and
A7: p2 in G by TOPS_1:22;
reconsider H = G as Subset of T1 by A1;
 G in the topology of T2 by A5, PRE_TOPC:def_2;
then  H is open by A1, PRE_TOPC:def_2;
then  p1 in Int W by A3, A6, A7, TOPS_1:22;
then reconsider W = V as a_neighborhood of p1 by CONNSP_2:def_1;
thus  N2 is_eventually_in V ::_thesis: verum
proof
 N1 is_eventually_in W by A4, YELLOW_6:def_15;
then consider i being Element of N1 such that
A8: for j being Element of N1 st i <= j holds
N1 . j in W by WAYBEL_0:def_11;
reconsider ii = i as Element of N2 by A2;
take  ii ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N2 holds
( not ii <= b1 or N2 . b1 in V )
let jj be Element of N2; ::_thesis: ( not ii <= jj or N2 . jj in V )
reconsider j = jj as Element of N1 by A2;
assume A9: ii <= jj ; ::_thesis: N2 . jj in V
 N2 . jj = N1 . j by A2;
hence  N2 . jj in V by A2, A8, A9; ::_thesis: verum
end;
end;
hence  p2 in Lim N2 by YELLOW_6:def_15; ::_thesis: verum
end;

Lm8:  for T1, T2 being non empty TopSpace st TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds
Convergence T1 = Convergence T2
proof
let T1, T2 be non empty TopSpace; ::_thesis: ( TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) implies Convergence T1 = Convergence T2 )
assume A1: TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) ; ::_thesis: Convergence T1 = Convergence T2
A2: Convergence T1 c= [:(NetUniv T1), the carrier of T1:] by YELLOW_6:def_18;
A3: Convergence T2 c= [:(NetUniv T2), the carrier of T2:] by YELLOW_6:def_18;
let u1, u2 be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [u1,u2] in Convergence T1 or [u1,u2] in Convergence T2 ) & ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 ) )
hereby  ::_thesis: ( not [u1,u2] in Convergence T2 or [u1,u2] in Convergence T1 )
assume A4: [u1,u2] in Convergence T1 ; ::_thesis: [u1,u2] in Convergence T2
then consider N1 being Element of NetUniv T1, p1 being Point of T1 such that
A5: [u1,u2] = [N1,p1] by A2, DOMAIN_1:1;
A6: N1 in NetUniv T1 ;
 ex N being strict net of T1 st
( N = N1 & the carrier of N in the_universe_of the carrier of T1 ) by YELLOW_6:def_11;
then reconsider N1 = N1 as net of T1 ;
A7: p1 in Lim N1 by A4, A5, YELLOW_6:def_19;
reconsider N2 = N1 as net of T2 by A1;
reconsider p2 = p1 as Point of T2 by A1;
A8: N2 in NetUniv T2 by A1, A6, Lm5;
 p2 in Lim N2 by A1, A7, Lm7;
hence  [u1,u2] in Convergence T2 by A5, A8, YELLOW_6:def_19; ::_thesis: verum
end;
assume A9: [u1,u2] in Convergence T2 ; ::_thesis: [u1,u2] in Convergence T1
then consider N1 being Element of NetUniv T2, p1 being Point of T2 such that
A10: [u1,u2] = [N1,p1] by A3, DOMAIN_1:1;
A11: N1 in NetUniv T2 ;
 ex N being strict net of T2 st
( N = N1 & the carrier of N in the_universe_of the carrier of T2 ) by YELLOW_6:def_11;
then reconsider N1 = N1 as net of T2 ;
A12: p1 in Lim N1 by A9, A10, YELLOW_6:def_19;
reconsider N2 = N1 as net of T1 by A1;
reconsider p2 = p1 as Point of T1 by A1;
A13: N2 in NetUniv T1 by A1, A11, Lm5;
 p2 in Lim N2 by A1, A12, Lm7;
hence  [u1,u2] in Convergence T1 by A10, A13, YELLOW_6:def_19; ::_thesis: verum
end;

Lm9:  for R1, R2 being non empty RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE holds
R2 is LATTICE
proof
let R1, R2 be non empty RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is LATTICE implies R2 is LATTICE )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: R1 is LATTICE ; ::_thesis: R2 is LATTICE
A3: R2 is with_infima
proof
let x, y be Element of R2; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of R2 holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A4: z9 <= x9 and
A5: z9 <= y9 and
A6: for w9 being Element of R1 st w9 <= x9 & w9 <= y9 holds
w9 <= z9 by A2, LATTICE3:def_11;
reconsider z = z9 as Element of R2 by A1;
take  z ; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
thus  ( z <= x & z <= y ) by A1, A4, A5, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds
( not b1 <= x or not b1 <= y or b1 <= z )
let w be Element of R2; ::_thesis: ( not w <= x or not w <= y or w <= z )
reconsider w9 = w as Element of R1 by A1;
assume that
A7: w <= x and
A8: w <= y ; ::_thesis: w <= z
A9: w9 <= x9 by A1, A7, Lm1;
 w9 <= y9 by A1, A8, Lm1;
then  w9 <= z9 by A6, A9;
hence  w <= z by A1, Lm1; ::_thesis: verum
end;
A10: R2 is with_suprema
proof
let x, y be Element of R2; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of R2 st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of R2 holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
reconsider x9 = x, y9 = y as Element of R1 by A1;
consider z9 being Element of R1 such that
A11: z9 >= x9 and
A12: z9 >= y9 and
A13: for w9 being Element of R1 st w9 >= x9 & w9 >= y9 holds
w9 >= z9 by A2, LATTICE3:def_10;
reconsider z = z9 as Element of R2 by A1;
take  z ; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
thus  ( z >= x & z >= y ) by A1, A11, A12, Lm1; ::_thesis: for b1 being Element of the carrier of R2 holds
( not x <= b1 or not y <= b1 or z <= b1 )
let w be Element of R2; ::_thesis: ( not x <= w or not y <= w or z <= w )
reconsider w9 = w as Element of R1 by A1;
assume that
A14: w >= x and
A15: w >= y ; ::_thesis: z <= w
A16: w9 >= x9 by A1, A14, Lm1;
 w9 >= y9 by A1, A15, Lm1;
then  w9 >= z9 by A13, A16;
hence  z <= w by A1, Lm1; ::_thesis: verum
end;
A17: R2 is reflexive
proof
let x be Element of R2; :: according to YELLOW_0:def_1 ::_thesis: x <= x
reconsider x9 = x as Element of R1 by A1;
 x9 <= x9 by A2, YELLOW_0:def_1;
hence  x <= x by A1, Lm1; ::_thesis: verum
end;
A18: R2 is transitive
proof
let x, y, z be Element of R2; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
reconsider x9 = x, y9 = y, z9 = z as Element of R1 by A1;
assume that
A19: x <= y and
A20: y <= z ; ::_thesis: x <= z
A21: x9 <= y9 by A1, A19, Lm1;
 y9 <= z9 by A1, A20, Lm1;
then  x9 <= z9 by A2, A21, YELLOW_0:def_2;
hence  x <= z by A1, Lm1; ::_thesis: verum
end;
 R2 is antisymmetric
proof
let x, y be Element of R2; :: according to YELLOW_0:def_3 ::_thesis: ( not x <= y or not y <= x or x = y )
reconsider x9 = x, y9 = y as Element of R1 by A1;
assume that
A22: x <= y and
A23: y <= x ; ::_thesis: x = y
A24: x9 <= y9 by A1, A22, Lm1;
 y9 <= x9 by A1, A23, Lm1;
hence  x = y by A2, A24, YELLOW_0:def_3; ::_thesis: verum
end;
hence  R2 is LATTICE by A3, A10, A17, A18; ::_thesis: verum
end;

Lm10:  for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
proof
let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_<=_than p1 holds
X is_<=_than p2
let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_<=_than p1 implies X is_<=_than p2 )
assume that
A2: p1 = p2 and
A3: X is_<=_than p1 ; ::_thesis: X is_<=_than p2
let b2 be Element of R2; :: according to LATTICE3:def_9 ::_thesis: ( not b2 in X or b2 <= p2 )
reconsider b1 = b2 as Element of R1 by A1;
assume  b2 in X ; ::_thesis: b2 <= p2
then  p1 >= b1 by A3, LATTICE3:def_9;
hence  b2 <= p2 by A1, A2, Lm1; ::_thesis: verum
end;

Lm11:  for R1, R2 being LATTICE
for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
proof
let R1, R2 be LATTICE; ::_thesis: for X being set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let X be set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p1 being Element of R1
for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p1 be Element of R1; ::_thesis: for p2 being Element of R2 st p1 = p2 & X is_>=_than p1 holds
X is_>=_than p2
let p2 be Element of R2; ::_thesis: ( p1 = p2 & X is_>=_than p1 implies X is_>=_than p2 )
assume that
A2: p1 = p2 and
A3: X is_>=_than p1 ; ::_thesis: X is_>=_than p2
let b2 be Element of R2; :: according to LATTICE3:def_8 ::_thesis: ( not b2 in X or p2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume  b2 in X ; ::_thesis: p2 <= b2
then  p1 <= b1 by A3, LATTICE3:def_8;
hence  p2 <= b2 by A1, A2, Lm1; ::_thesis: verum
end;

Lm12:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "\/" (D,R1) = "\/" (D,R2)
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "\/" (D,R1) = "\/" (D,R2) )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "\/" (D,R1) = "\/" (D,R2)
let D be set ; ::_thesis: "\/" (D,R1) = "\/" (D,R2)
reconsider b = "\/" (D,R1) as Element of R2 by A1;
A2: ex_sup_of D,R2 by YELLOW_0:17;
A3: ex_sup_of D,R1 by YELLOW_0:17;
then  D is_<=_than "\/" (D,R1) by YELLOW_0:def_9;
then A4: D is_<=_than b by A1, Lm10;
 for a being Element of R2 st D is_<=_than a holds
a >= b
proof
let a be Element of R2; ::_thesis: ( D is_<=_than a implies a >= b )
reconsider a9 = a as Element of R1 by A1;
assume  D is_<=_than a ; ::_thesis: a >= b
then  D is_<=_than a9 by A1, Lm10;
then  a9 >= "\/" (D,R1) by A3, YELLOW_0:def_9;
hence  a >= b by A1, Lm1; ::_thesis: verum
end;
hence  "\/" (D,R1) = "\/" (D,R2) by A2, A4, YELLOW_0:def_9; ::_thesis: verum
end;

Lm13:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being set holds "/\" (D,R1) = "/\" (D,R2)
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being set holds "/\" (D,R1) = "/\" (D,R2) )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being set holds "/\" (D,R1) = "/\" (D,R2)
let D be set ; ::_thesis: "/\" (D,R1) = "/\" (D,R2)
reconsider b = "/\" (D,R1) as Element of R2 by A1;
A2: ex_inf_of D,R2 by YELLOW_0:17;
A3: ex_inf_of D,R1 by YELLOW_0:17;
then  D is_>=_than "/\" (D,R1) by YELLOW_0:def_10;
then A4: D is_>=_than b by A1, Lm11;
 for a being Element of R2 st D is_>=_than a holds
a <= b
proof
let a be Element of R2; ::_thesis: ( D is_>=_than a implies a <= b )
reconsider a9 = a as Element of R1 by A1;
assume  D is_>=_than a ; ::_thesis: a <= b
then  D is_>=_than a9 by A1, Lm11;
then  a9 <= "/\" (D,R1) by A3, YELLOW_0:def_10;
hence  a <= b by A1, Lm1; ::_thesis: verum
end;
hence  "/\" (D,R1) = "/\" (D,R2) by A2, A4, YELLOW_0:def_10; ::_thesis: verum
end;

Lm14:  for R1, R2 being non empty reflexive RelStr st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D be Subset of R1; ::_thesis: for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D9 be Subset of R2; ::_thesis: ( D = D9 & D is directed implies D9 is directed )
assume that
A2: D = D9 and
A3: D is directed ; ::_thesis: D9 is directed
let x2, y2 be Element of R2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x2 in D9 or not y2 in D9 or ex b1 being Element of the carrier of R2 st
( b1 in D9 & x2 <= b1 & y2 <= b1 ) )
assume that
A4: x2 in D9 and
A5: y2 in D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 in D9 & x2 <= b1 & y2 <= b1 )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
consider z1 being Element of R1 such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2, A3, A4, A5, WAYBEL_0:def_1;
reconsider z2 = z1 as Element of R2 by A1;
take  z2 ; ::_thesis: ( z2 in D9 & x2 <= z2 & y2 <= z2 )
thus  z2 in D9 by A2, A6; ::_thesis: ( x2 <= z2 & y2 <= z2 )
thus  ( x2 <= z2 & y2 <= z2 ) by A1, A7, A8, Lm1; ::_thesis: verum
end;

Lm15:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for p, q being Element of R1 st p << q holds
for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p, q be Element of R1; ::_thesis: ( p << q implies for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9 )
assume A2: p << q ; ::_thesis: for p9, q9 being Element of R2 st p = p9 & q = q9 holds
p9 << q9
let p9, q9 be Element of R2; ::_thesis: ( p = p9 & q = q9 implies p9 << q9 )
assume that
A3: p = p9 and
A4: q = q9 ; ::_thesis: p9 << q9
let D9 be non empty directed Subset of R2; :: according to WAYBEL_3:def_1 ::_thesis: ( not q9 <= "\/" (D9,R2) or ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 ) )
assume A5: q9 <= sup D9 ; ::_thesis: ex b1 being Element of the carrier of R2 st
( b1 in D9 & p9 <= b1 )
reconsider D = D9 as non empty Subset of R1 by A1;
reconsider D = D as non empty directed Subset of R1 by A1, Lm14;
 sup D = sup D9 by A1, Lm12;
then  q <= sup D by A1, A4, A5, Lm1;
then consider d being Element of R1 such that
A6: d in D and
A7: p <= d by A2, WAYBEL_3:def_1;
reconsider d9 = d as Element of R2 by A1;
take  d9 ; ::_thesis: ( d9 in D9 & p9 <= d9 )
thus  d9 in D9 by A6; ::_thesis: p9 <= d9
thus  p9 <= d9 by A1, A3, A7, Lm1; ::_thesis: verum
end;

Lm16:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
lim_inf N1 = lim_inf N2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies lim_inf N1 = lim_inf N2 )
assume A2: N1 = N2 ; ::_thesis: lim_inf N1 = lim_inf N2
set X1 =  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  ;
set X2 =  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  ;
  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  =  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }
proof
thus   {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  c=  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  c=  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  or e in  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  )
assume  e in  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  ; ::_thesis: e in  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }
then consider j1 being Element of N1 such that
A3: e = "/\" ( {  (N1 . i) where i is Element of N1 : i >= j1  }  ,R1) ;
reconsider j2 = j1 as Element of N2 by A2;
set Y1 =  {  (N1 . i) where i is Element of N1 : i >= j1  }  ;
set Y2 =  {  (N2 . i) where i is Element of N2 : i >= j2  }  ;
  {  (N1 . i) where i is Element of N1 : i >= j1  }  =  {  (N2 . i) where i is Element of N2 : i >= j2  }
proof
thus   {  (N1 . i) where i is Element of N1 : i >= j1  }  c=  {  (N2 . i) where i is Element of N2 : i >= j2  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (N2 . i) where i is Element of N2 : i >= j2  }  c=  {  (N1 . i) where i is Element of N1 : i >= j1  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (N1 . i) where i is Element of N1 : i >= j1  }  or u in  {  (N2 . i) where i is Element of N2 : i >= j2  }  )
assume  u in  {  (N1 . i) where i is Element of N1 : i >= j1  }  ; ::_thesis: u in  {  (N2 . i) where i is Element of N2 : i >= j2  }
then consider i1 being Element of N1 such that
A4: u = N1 . i1 and
A5: j1 <= i1 ;
reconsider i2 = i1 as Element of N2 by A2;
 N2 . i2 = u by A2, A4;
hence  u in  {  (N2 . i) where i is Element of N2 : i >= j2  }  by A2, A5; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (N2 . i) where i is Element of N2 : i >= j2  }  or u in  {  (N1 . i) where i is Element of N1 : i >= j1  }  )
assume  u in  {  (N2 . i) where i is Element of N2 : i >= j2  }  ; ::_thesis: u in  {  (N1 . i) where i is Element of N1 : i >= j1  }
then consider i2 being Element of N2 such that
A6: u = N2 . i2 and
A7: j2 <= i2 ;
reconsider i1 = i2 as Element of N1 by A2;
 N1 . i1 = u by A2, A6;
hence  u in  {  (N1 . i) where i is Element of N1 : i >= j1  }  by A2, A7; ::_thesis: verum
end;
then  e = "/\" ( {  (N2 . i) where i is Element of N2 : i >= j2  }  ,R2) by A1, A3, Lm13;
hence  e in  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  or e in  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  )
assume  e in  {  ("/\" ( {  (N2 . i) where i is Element of N2 : i >= j  }  ,R2)) where j is Element of N2 : verum  }  ; ::_thesis: e in  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }
then consider j1 being Element of N2 such that
A8: e = "/\" ( {  (N2 . i) where i is Element of N2 : i >= j1  }  ,R2) ;
reconsider j2 = j1 as Element of N1 by A2;
set Y1 =  {  (N2 . i) where i is Element of N2 : i >= j1  }  ;
set Y2 =  {  (N1 . i) where i is Element of N1 : i >= j2  }  ;
  {  (N2 . i) where i is Element of N2 : i >= j1  }  =  {  (N1 . i) where i is Element of N1 : i >= j2  }
proof
thus   {  (N2 . i) where i is Element of N2 : i >= j1  }  c=  {  (N1 . i) where i is Element of N1 : i >= j2  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (N1 . i) where i is Element of N1 : i >= j2  }  c=  {  (N2 . i) where i is Element of N2 : i >= j1  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (N2 . i) where i is Element of N2 : i >= j1  }  or u in  {  (N1 . i) where i is Element of N1 : i >= j2  }  )
assume  u in  {  (N2 . i) where i is Element of N2 : i >= j1  }  ; ::_thesis: u in  {  (N1 . i) where i is Element of N1 : i >= j2  }
then consider i1 being Element of N2 such that
A9: u = N2 . i1 and
A10: j1 <= i1 ;
reconsider i2 = i1 as Element of N1 by A2;
 N1 . i2 = u by A2, A9;
hence  u in  {  (N1 . i) where i is Element of N1 : i >= j2  }  by A2, A10; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (N1 . i) where i is Element of N1 : i >= j2  }  or u in  {  (N2 . i) where i is Element of N2 : i >= j1  }  )
assume  u in  {  (N1 . i) where i is Element of N1 : i >= j2  }  ; ::_thesis: u in  {  (N2 . i) where i is Element of N2 : i >= j1  }
then consider i2 being Element of N1 such that
A11: u = N1 . i2 and
A12: j2 <= i2 ;
reconsider i1 = i2 as Element of N2 by A2;
 N2 . i1 = u by A2, A11;
hence  u in  {  (N2 . i) where i is Element of N2 : i >= j1  }  by A2, A12; ::_thesis: verum
end;
then  e = "/\" ( {  (N1 . i) where i is Element of N1 : i >= j2  }  ,R1) by A1, A8, Lm13;
hence  e in  {  ("/\" ( {  (N1 . i) where i is Element of N1 : i >= j  }  ,R1)) where j is Element of N1 : verum  }  ; ::_thesis: verum
end;
hence  lim_inf N1 = lim_inf N2 by A1, Lm12; ::_thesis: verum
end;

Lm17:  for R1, R2 being non empty reflexive RelStr
for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let X be non empty set ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2 )
assume A1: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1
for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J1 be net_set of the carrier of N1,R1; ::_thesis: for J2 being net_set of the carrier of N2,R2 st J1 = J2 holds
Iterated J1 = Iterated J2
let J2 be net_set of the carrier of N2,R2; ::_thesis: ( J1 = J2 implies Iterated J1 = Iterated J2 )
assume A2: J1 = J2 ; ::_thesis: Iterated J1 = Iterated J2
A3: RelStr(# the carrier of (Iterated J1), the InternalRel of (Iterated J1) #) = [:N1,(product J1):] by YELLOW_6:def_13;
A4: RelStr(# the carrier of (Iterated J2), the InternalRel of (Iterated J2) #) = [:N2,(product J2):] by YELLOW_6:def_13;
set f = the mapping of (Iterated J1);
set g = the mapping of (Iterated J2);
A5: dom the mapping of (Iterated J1) = the carrier of (Iterated J2) by A1, A2, A3, A4, FUNCT_2:def_1
.= dom the mapping of (Iterated J2) by FUNCT_2:def_1 ;
 for x being set st x in dom the mapping of (Iterated J1) holds
the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x
proof
let x be set ; ::_thesis: ( x in dom the mapping of (Iterated J1) implies the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x )
assume  x in dom the mapping of (Iterated J1) ; ::_thesis: the mapping of (Iterated J1) . x = the mapping of (Iterated J2) . x
then  x in the carrier of (Iterated J1) ;
then  x in [: the carrier of N1, the carrier of (product J1):] by A3, YELLOW_3:def_2;
then consider x1 being Element of N1, x2 being Element of (product J1) such that
A6: x = [x1,x2] by DOMAIN_1:1;
reconsider y1 = x1 as Element of N2 by A1;
reconsider y2 = x2 as Element of (product J2) by A1, A2;
thus  the mapping of (Iterated J1) . x = the mapping of (Iterated J1) . (x1,x2) by A6
.= the mapping of (J1 . x1) . (x2 . x1) by YELLOW_6:def_13
.= the mapping of (J2 . y1) . (y2 . y1) by A2
.= the mapping of (Iterated J2) . (y1,y2) by YELLOW_6:def_13
.= the mapping of (Iterated J2) . x by A6 ; ::_thesis: verum
end;
then  the mapping of (Iterated J1) = the mapping of (Iterated J2) by A5, FUNCT_1:2;
hence  Iterated J1 = Iterated J2 by A1, A2, A3, A4; ::_thesis: verum
end;

Lm18:  for R1, R2 being non empty reflexive RelStr
for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
proof
let R1, R2 be non empty reflexive RelStr ; ::_thesis: for X being non empty set st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let X be non empty set ; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: for N1 being net of R1
for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N1 be net of R1; ::_thesis: for N2 being net of R2 st N1 = N2 holds
for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let N2 be net of R2; ::_thesis: ( N1 = N2 implies for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2 )
assume A2: N1 = N2 ; ::_thesis: for J1 being net_set of the carrier of N1,R1 holds J1 is net_set of the carrier of N2,R2
let J1 be net_set of the carrier of N1,R1; ::_thesis: J1 is net_set of the carrier of N2,R2
reconsider J2 = J1 as ManySortedSet of the carrier of N2 by A2;
 for i being set st i in rng J2 holds
i is net of R2
proof
let i be set ; ::_thesis: ( i in rng J2 implies i is net of R2 )
assume  i in rng J2 ; ::_thesis: i is net of R2
then reconsider N = i as net of R1 by YELLOW_6:def_12;
 N is NetStr over R2 by A1;
hence  i is net of R2 ; ::_thesis: verum
end;
hence  J1 is net_set of the carrier of N2,R2 by YELLOW_6:def_12; ::_thesis: verum
end;

Lm19:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 c= Scott-Convergence R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 c= Scott-Convergence R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 c= Scott-Convergence R2
A2: Scott-Convergence R1 c= [:(NetUniv R1), the carrier of R1:] by YELLOW_6:def_18;
 for e being set st e in Scott-Convergence R1 holds
e in Scott-Convergence R2
proof
let e be set ; ::_thesis: ( e in Scott-Convergence R1 implies e in Scott-Convergence R2 )
assume A3: e in Scott-Convergence R1 ; ::_thesis: e in Scott-Convergence R2
then consider N1 being Element of NetUniv R1, p1 being Element of R1 such that
A4: e = [N1,p1] by A2, DOMAIN_1:1;
A5: N1 in NetUniv R1 ;
A6: ex N being strict net of R1 st
( N1 = N & the carrier of N in the_universe_of the carrier of R1 ) by YELLOW_6:def_11;
then reconsider N2 = N1 as strict net of R2 by A1, Lm4;
reconsider N1 = N1 as strict net of R1 by A6;
reconsider p2 = p1 as Element of R2 by A1;
A7: N2 in NetUniv R2 by A1, A5, Lm5;
A8: lim_inf N1 = lim_inf N2 by A1, Lm16;
 p1 is_S-limit_of N1 by A3, A4, Def8;
then  p1 <= lim_inf N1 by Def7;
then  p2 <= lim_inf N2 by A1, A8, Lm1;
then  p2 is_S-limit_of N2 by Def7;
hence  e in Scott-Convergence R2 by A4, A7, Def8; ::_thesis: verum
end;
hence  Scott-Convergence R1 c= Scott-Convergence R2 by TARSKI:def_3; ::_thesis: verum
end;

Lm20:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
Scott-Convergence R1 = Scott-Convergence R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies Scott-Convergence R1 = Scott-Convergence R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: Scott-Convergence R1 = Scott-Convergence R2
then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19;
 Scott-Convergence R2 c= Scott-Convergence R1 by A1, Lm19;
hence  Scott-Convergence R1 = Scott-Convergence R2 by A2, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm21:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) holds
sigma R1 = sigma R2
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies sigma R1 = sigma R2 )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: sigma R1 = sigma R2
set T1 = ConvergenceSpace (Scott-Convergence R1);
set T2 = ConvergenceSpace (Scott-Convergence R2);
A2: the topology of (ConvergenceSpace (Scott-Convergence R1)) =  {  V where V is Subset of R1 : for p being Element of R1 st p in V holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V  }  by YELLOW_6:def_24;
A3: the topology of (ConvergenceSpace (Scott-Convergence R2)) =  {  V where V is Subset of R2 : for p being Element of R2 st p in V holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V  }  by YELLOW_6:def_24;
 the topology of (ConvergenceSpace (Scott-Convergence R1)) = the topology of (ConvergenceSpace (Scott-Convergence R2))
proof
thus  the topology of (ConvergenceSpace (Scott-Convergence R1)) c= the topology of (ConvergenceSpace (Scott-Convergence R2)) :: according to XBOOLE_0:def_10 ::_thesis: the topology of (ConvergenceSpace (Scott-Convergence R2)) c= the topology of (ConvergenceSpace (Scott-Convergence R1))
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R1)) or e in the topology of (ConvergenceSpace (Scott-Convergence R2)) )
assume  e in the topology of (ConvergenceSpace (Scott-Convergence R1)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R2))
then consider V1 being Subset of R1 such that
A4: e = V1 and
A5: for p being Element of R1 st p in V1 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V1 by A2;
reconsider V2 = V1 as Subset of R2 by A1;
 for p being Element of R2 st p in V2 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V2
proof
let p2 be Element of R2; ::_thesis: ( p2 in V2 implies for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2 )
assume A6: p2 in V2 ; ::_thesis: for N being net of R2 st [N,p2] in Scott-Convergence R2 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R1 by A1;
let N2 be net of R2; ::_thesis: ( [N2,p2] in Scott-Convergence R2 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R1 by A1;
assume  [N2,p2] in Scott-Convergence R2 ; ::_thesis: N2 is_eventually_in V2
then  [N1,p1] in Scott-Convergence R1 by A1, Lm20;
hence  N2 is_eventually_in V2 by A5, A6, Lm6; ::_thesis: verum
end;
hence  e in the topology of (ConvergenceSpace (Scott-Convergence R2)) by A3, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in the topology of (ConvergenceSpace (Scott-Convergence R2)) or e in the topology of (ConvergenceSpace (Scott-Convergence R1)) )
assume  e in the topology of (ConvergenceSpace (Scott-Convergence R2)) ; ::_thesis: e in the topology of (ConvergenceSpace (Scott-Convergence R1))
then consider V1 being Subset of R2 such that
A7: e = V1 and
A8: for p being Element of R2 st p in V1 holds
for N being net of R2 st [N,p] in Scott-Convergence R2 holds
N is_eventually_in V1 by A3;
reconsider V2 = V1 as Subset of R1 by A1;
 for p being Element of R1 st p in V2 holds
for N being net of R1 st [N,p] in Scott-Convergence R1 holds
N is_eventually_in V2
proof
let p2 be Element of R1; ::_thesis: ( p2 in V2 implies for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2 )
assume A9: p2 in V2 ; ::_thesis: for N being net of R1 st [N,p2] in Scott-Convergence R1 holds
N is_eventually_in V2
reconsider p1 = p2 as Element of R2 by A1;
let N2 be net of R1; ::_thesis: ( [N2,p2] in Scott-Convergence R1 implies N2 is_eventually_in V2 )
reconsider N1 = N2 as net of R2 by A1;
assume  [N2,p2] in Scott-Convergence R1 ; ::_thesis: N2 is_eventually_in V2
then  [N1,p1] in Scott-Convergence R2 by A1, Lm20;
hence  N2 is_eventually_in V2 by A8, A9, Lm6; ::_thesis: verum
end;
hence  e in the topology of (ConvergenceSpace (Scott-Convergence R1)) by A2, A7; ::_thesis: verum
end;
hence  sigma R1 = sigma R2 ; ::_thesis: verum
end;

Lm22:  for R1, R2 being LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete holds
R2 is complete
proof
let R1, R2 be LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is complete implies R2 is complete )
assume that
A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) and
A2: R1 is complete ; ::_thesis: R2 is complete
let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of R2 st
( X is_<=_than b1 & ( for b2 being Element of the carrier of R2 holds
( not X is_<=_than b2 or b1 <= b2 ) ) )
consider a1 being Element of R1 such that
A3: X is_<=_than a1 and
A4: for b being Element of R1 st X is_<=_than b holds
a1 <= b by A2, LATTICE3:def_12;
reconsider a2 = a1 as Element of R2 by A1;
take  a2 ; ::_thesis: ( X is_<=_than a2 & ( for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 ) ) )
thus  X is_<=_than a2 by A1, A3, Lm10; ::_thesis: for b1 being Element of the carrier of R2 holds
( not X is_<=_than b1 or a2 <= b1 )
let b2 be Element of R2; ::_thesis: ( not X is_<=_than b2 or a2 <= b2 )
reconsider b1 = b2 as Element of R1 by A1;
assume  X is_<=_than b2 ; ::_thesis: a2 <= b2
then  X is_<=_than b1 by A1, Lm10;
hence  a2 <= b2 by A1, A4, Lm1; ::_thesis: verum
end;

Lm23:  for R1, R2 being complete LATTICE st RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous holds
R2 is continuous
proof
let R1, R2 be complete LATTICE; ::_thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) & R1 is continuous implies R2 is continuous )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; ::_thesis: ( not R1 is continuous or R2 is continuous )
assume A2: R1 is continuous ; ::_thesis: R2 is continuous
thus A3: for x being Element of R2 holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( R2 is up-complete & R2 is satisfying_axiom_of_approximation )
thus  R2 is up-complete ; ::_thesis: R2 is satisfying_axiom_of_approximation
A4: for x being Element of R1 holds
( not waybelow x is empty & waybelow x is directed ) ;
 for x, y being Element of R2 st not x <= y holds
ex u being Element of R2 st
( u << x & not u <= y )
proof
let x2, y2 be Element of R2; ::_thesis: ( not x2 <= y2 implies ex u being Element of R2 st
( u << x2 & not u <= y2 ) )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
assume  not x2 <= y2 ; ::_thesis: ex u being Element of R2 st
( u << x2 & not u <= y2 )
then  not x1 <= y1 by A1, Lm1;
then consider u1 being Element of R1 such that
A5: u1 << x1 and
A6: not u1 <= y1 by A2, A4, WAYBEL_3:24;
reconsider u2 = u1 as Element of R2 by A1;
take  u2 ; ::_thesis: ( u2 << x2 & not u2 <= y2 )
thus  u2 << x2 by A1, A5, Lm15; ::_thesis: not u2 <= y2
thus  not u2 <= y2 by A1, A6, Lm1; ::_thesis: verum
end;
hence  R2 is satisfying_axiom_of_approximation by A3, WAYBEL_3:24; ::_thesis: verum
end;

registration
let R be complete continuous LATTICE;
cluster Scott-Convergence R ->  topological ;
coherence
 Scott-Convergence R is topological
proof
set C = Scott-Convergence R;
thus  ( Scott-Convergence R is (CONSTANTS) & Scott-Convergence R is (SUBNETS) ) ; :: according to YELLOW_6:def_25 ::_thesis: ( Scott-Convergence R is (DIVERGENCE) & Scott-Convergence R is (ITERATED_LIMITS) )
thus  Scott-Convergence R is (DIVERGENCE) ::_thesis: Scott-Convergence R is (ITERATED_LIMITS)
proof
let X be net of R; :: according to YELLOW_6:def_22 ::_thesis: for b1 being Element of the carrier of R holds
( not X in NetUniv R or [X,b1] in Scott-Convergence R or ex b2 being subnet of X st
( b2 in NetUniv R & ( for b3 being subnet of b2 holds not [b3,b1] in Scott-Convergence R ) ) )
let p be Element of R; ::_thesis: ( not X in NetUniv R or [X,p] in Scott-Convergence R or ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) ) )
assume that
A1: X in NetUniv R and
A2: not [X,p] in Scott-Convergence R ; ::_thesis: ex b1 being subnet of X st
( b1 in NetUniv R & ( for b2 being subnet of b1 holds not [b2,p] in Scott-Convergence R ) )
A3: for x being Element of R holds
( not waybelow x is empty & waybelow x is directed ) ;
reconsider p9 = p as Element of R ;
consider N being strict net of R such that
A4: N = X and
 the carrier of N in the_universe_of the carrier of R by A1, YELLOW_6:def_11;
 not p is_S-limit_of N by A1, A2, A4, Def8;
then  not p <= lim_inf X by A4, Def7;
then consider u being Element of R such that
A5: u << p9 and
A6: not u <= lim_inf X by A3, WAYBEL_3:24;
set A =  {  a where a is Element of R : not a >= u  }  ;
 X is_often_in  {  a where a is Element of R : not a >= u  }
proof
let i be Element of X; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of X st
( i <= b1 & X . b1 in  {  a where a is Element of R : not a >= u  }  )
set B =  {  (X . j) where j is Element of X : j >= i  }  ;
set C =  {  ("/\" ( {  (X . k) where k is Element of X : k >= j  }  ,R)) where j is Element of X : verum  }  ;
 "/\" ( {  (X . j) where j is Element of X : j >= i  }  ,R) in  {  ("/\" ( {  (X . k) where k is Element of X : k >= j  }  ,R)) where j is Element of X : verum  }  ;
then  "/\" ( {  (X . j) where j is Element of X : j >= i  }  ,R) <= lim_inf X by YELLOW_2:22;
then  not u <= "/\" ( {  (X . j) where j is Element of X : j >= i  }  ,R) by A6, YELLOW_0:def_2;
then  not u is_<=_than  {  (X . j) where j is Element of X : j >= i  }  by YELLOW_0:33;
then consider b being Element of R such that
A7: b in  {  (X . j) where j is Element of X : j >= i  }  and
A8: not u <= b by LATTICE3:def_8;
consider j being Element of X such that
A9: b = X . j and
A10: j >= i by A7;
take  j ; ::_thesis: ( i <= j & X . j in  {  a where a is Element of R : not a >= u  }  )
thus  i <= j by A10; ::_thesis: X . j in  {  a where a is Element of R : not a >= u  }
thus  X . j in  {  a where a is Element of R : not a >= u  }  by A8, A9; ::_thesis: verum
end;
then reconsider Y = X "  {  a where a is Element of R : not a >= u  }  as subnet of X by YELLOW_6:22;
take  Y ; ::_thesis: ( Y in NetUniv R & ( for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R ) )
reconsider UN = the_universe_of the carrier of R as universal set ;
A11: ex N being strict net of R st
( X = N & the carrier of N in UN ) by A1, YELLOW_6:def_11;
 X "  {  a where a is Element of R : not a >= u  }  is SubRelStr of X by YELLOW_6:def_6;
then  the carrier of (X "  {  a where a is Element of R : not a >= u  }  ) c= the carrier of X by YELLOW_0:def_13;
then  the carrier of Y in UN by A11, CLASSES1:def_1;
hence  Y in NetUniv R by YELLOW_6:def_11; ::_thesis: for b1 being subnet of Y holds not [b1,p] in Scott-Convergence R
let Z be subnet of Y; ::_thesis: not [Z,p] in Scott-Convergence R
assume A12: [Z,p] in Scott-Convergence R ; ::_thesis: contradiction
 Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A13: Z in NetUniv R by A12, ZFMISC_1:87;
then consider ZZ being strict net of R such that
A14: ZZ = Z and
 the carrier of ZZ in UN by YELLOW_6:def_11;
deffunc H1( Element of Z) ->  Element of the carrier of R = "/\" ( {  (Z . i) where i is Element of Z : i >= R  }  ,R);
defpred S1[ set ] means verum;
set D =  {  H1(j) where j is Element of Z : S1[j]  }  ;
  {  H1(j) where j is Element of Z : S1[j]  }  is Subset of R from DOMAIN_1:sch_8();
then reconsider D =  {  H1(j) where j is Element of Z : S1[j]  }  as Subset of R ;
reconsider D = D as non empty directed Subset of R by Th30;
 p is_S-limit_of ZZ by A12, A13, A14, Def8;
then  p <= lim_inf Z by A14, Def7;
then consider d being Element of R such that
A15: d in D and
A16: u <= d by A5, WAYBEL_3:def_1;
consider j being Element of Z such that
A17: d = "/\" ( {  (Z . k) where k is Element of Z : k >= j  }  ,R) by A15;
reconsider j9 = j as Element of Z ;
consider i being Element of Z such that
A18: i >= j9 and
 i >= j9 by YELLOW_6:def_3;
consider f being Function of Z,Y such that
A19: the mapping of Z = the mapping of Y * f and
 for m being Element of Y ex n being Element of Z st
for p being Element of Z st n <= p holds
m <= f . p by YELLOW_6:def_9;
 Z . i in  {  (Z . k) where k is Element of Z : k >= j  }  by A18;
then A20: d <= Z . i by A17, YELLOW_2:22;
 Y . (f . i) = Z . i by A19, FUNCT_2:15;
then  Z . i in  {  a where a is Element of R : not a >= u  }  by Th35;
then  ex a being Element of R st
( a = Z . i & not a >= u ) ;
hence  contradiction by A16, A20, YELLOW_0:def_2; ::_thesis: verum
end;
thus  Scott-Convergence R is (ITERATED_LIMITS) ::_thesis: verum
proof
let X be net of R; :: according to YELLOW_6:def_23 ::_thesis: for b1 being Element of the carrier of R holds
( not [X,b1] in Scott-Convergence R or for b2 being net_set of the carrier of X,R holds
( ex b3 being Element of the carrier of X st not [(b2 . b3),(X . b3)] in Scott-Convergence R or [(Iterated b2),b1] in Scott-Convergence R ) )
let p be Element of R; ::_thesis: ( not [X,p] in Scott-Convergence R or for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R ) )
assume A21: [X,p] in Scott-Convergence R ; ::_thesis: for b1 being net_set of the carrier of X,R holds
( ex b2 being Element of the carrier of X st not [(b1 . b2),(X . b2)] in Scott-Convergence R or [(Iterated b1),p] in Scott-Convergence R )
let J be net_set of the carrier of X,R; ::_thesis: ( ex b1 being Element of the carrier of X st not [(J . b1),(X . b1)] in Scott-Convergence R or [(Iterated J),p] in Scott-Convergence R )
assume A22: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence R ; ::_thesis: [(Iterated J),p] in Scott-Convergence R
A23: Scott-Convergence R c= [:(NetUniv R), the carrier of R:] by YELLOW_6:def_18;
then A24: X in NetUniv R by A21, ZFMISC_1:87;
 for i being Element of X holds J . i in NetUniv R
proof
let i be Element of X; ::_thesis: J . i in NetUniv R
 [(J . i),(X . i)] in Scott-Convergence R by A22;
hence  J . i in NetUniv R by A23, ZFMISC_1:87; ::_thesis: verum
end;
then A25: Iterated J in NetUniv R by A24, YELLOW_6:25;
reconsider p9 = p as Element of R ;
set q = lim_inf (Iterated J);
 lim_inf (Iterated J) is_>=_than waybelow p9
proof
let u be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not u in waybelow p9 or u <= lim_inf (Iterated J) )
assume  u in waybelow p9 ; ::_thesis: u <= lim_inf (Iterated J)
then A26: u << p9 by WAYBEL_3:7;
set T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #);
A27: 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 #) ;
A28: the carrier of R = the carrier of (ConvergenceSpace (Scott-Convergence R)) by YELLOW_6:def_24;
then reconsider T = TopRelStr(# the carrier of R, the InternalRel of R,(sigma R) #) as TopLattice by A27, Lm3, Lm9;
reconsider T = T as complete TopLattice by A27, Lm22;
reconsider T = T as complete continuous TopLattice by A27, Lm23;
 the topology of T = sigma T by A27, Lm21;
then reconsider T = T as complete continuous Scott TopLattice by Th37;
reconsider XX = X as net of T ;
reconsider JJ = J as net_set of the carrier of XX,T by A27, Lm18;
reconsider uu = u, qq = lim_inf (Iterated J), pp = p9 as Element of T ;
set N = Iterated JJ;
set CC = Convergence T;
 Convergence T = Convergence (ConvergenceSpace (Scott-Convergence R)) by A28, Lm8;
then A29: Scott-Convergence R c= Convergence T by YELLOW_6:40;
A30: uu << pp by A26, A27, Lm15;
A31: qq = lim_inf (Iterated JJ) by A27, Lm16, Lm17;
 for i being Element of XX holds [(JJ . i),(XX . i)] in Convergence T
proof
let i be Element of XX; ::_thesis: [(JJ . i),(XX . i)] in Convergence T
reconsider ii = i as Element of X ;
 [(J . ii),(X . ii)] in Scott-Convergence R by A22;
hence  [(JJ . i),(XX . i)] in Convergence T by A29; ::_thesis: verum
end;
then  [(Iterated JJ),pp] in Convergence T by A21, A29, YELLOW_6:def_23;
then A32: pp in Lim (Iterated JJ) by YELLOW_6:def_19;
 pp in wayabove uu by A30;
then  wayabove uu is a_neighborhood of pp by Th36, CONNSP_2:3;
then A33: Iterated JJ is_eventually_in wayabove uu by A32, YELLOW_6:def_15;
 wayabove uu c= uparrow uu by WAYBEL_3:11;
then  Iterated JJ is_eventually_in uparrow uu by A33, WAYBEL_0:8;
hence  u <= lim_inf (Iterated J) by A27, A31, Lm1, Th18; ::_thesis: verum
end;
then  sup (waybelow p9) <= lim_inf (Iterated J) by YELLOW_0:32;
then  p <= lim_inf (Iterated J) by WAYBEL_3:def_5;
then  p is_S-limit_of Iterated J by Def7;
hence  [(Iterated J),p] in Scott-Convergence R by A25, Def8; ::_thesis: verum
end;
end;
end;

theorem :: WAYBEL11:38
for T being complete continuous Scott TopLattice
for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
proof
let T be complete continuous Scott TopLattice; ::_thesis: for x being Element of T
for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let x be Element of T; ::_thesis: for N being net of T st N in NetUniv T holds
( x is_S-limit_of N iff x in Lim N )
let N be net of T; ::_thesis: ( N in NetUniv T implies ( x is_S-limit_of N iff x in Lim N ) )
assume A1: N in NetUniv T ; ::_thesis: ( x is_S-limit_of N iff x in Lim N )
A2: Convergence (ConvergenceSpace (Scott-Convergence T)) = Scott-Convergence T by YELLOW_6:44;
consider M being strict net of T such that
A3: M = N and
 the carrier of M in the_universe_of the carrier of T by A1, YELLOW_6:def_11;
 TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
then A4: Convergence T = Convergence (ConvergenceSpace (Scott-Convergence T)) by Lm8;
thus  ( x is_S-limit_of N implies x in Lim N ) ::_thesis: ( x in Lim N implies x is_S-limit_of N )
proof
assume  x is_S-limit_of N ; ::_thesis: x in Lim N
then  [N,x] in Convergence T by A1, A2, A3, A4, Def8;
hence  x in Lim N by YELLOW_6:def_19; ::_thesis: verum
end;
assume  x in Lim N ; ::_thesis: x is_S-limit_of N
then  [M,x] in Scott-Convergence T by A1, A2, A3, A4, YELLOW_6:def_19;
hence  x is_S-limit_of N by A1, A3, Def8; ::_thesis: verum
end;

theorem Th39: :: WAYBEL11:39
for L being non empty complete Poset st Scott-Convergence L is (ITERATED_LIMITS) holds
L is continuous
proof
let L be non empty complete Poset; ::_thesis: ( Scott-Convergence L is (ITERATED_LIMITS) implies L is continuous )
assume A1: Scott-Convergence L is (ITERATED_LIMITS) ; ::_thesis: L is continuous
set C = Scott-Convergence L;
now__::_thesis:_for_I_being_non_empty_set_st_I_in_the_universe_of_the_carrier_of_L_holds_
for_K_being_V8()_ManySortedSet_of_I_st_(_for_j_being_Element_of_I_holds_K_._j_in_the_universe_of_the_carrier_of_L_)_holds_
for_F_being_DoubleIndexedSet_of_K,L_st_(_for_j_being_Element_of_I_holds_rng_(F_._j)_is_directed_)_holds_
Inf_=_Sup
let I be non empty set ; ::_thesis: ( I in the_universe_of the carrier of L implies for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )
assume A2: I in the_universe_of the carrier of L ; ::_thesis: for K being V8() ManySortedSet of I st ( for j being Element of I holds K . j in the_universe_of the carrier of L ) holds
for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup
let K be V8() ManySortedSet of I; ::_thesis: ( ( for j being Element of I holds K . j in the_universe_of the carrier of L ) implies for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup )
assume A3: for j being Element of I holds K . j in the_universe_of the carrier of L ; ::_thesis: for F being DoubleIndexedSet of K,L st ( for j being Element of I holds rng (F . j) is directed ) holds
Inf = Sup
let F be DoubleIndexedSet of K,L; ::_thesis: ( ( for j being Element of I holds rng (F . j) is directed ) implies Inf = Sup )
assume A4: for j being Element of I holds rng (F . j) is directed ; ::_thesis: Inf = Sup
set x = Inf ;
A5: Inf >= Sup by WAYBEL_5:16;
 [:I,I:] c= [:I,I:] ;
then reconsider r = [:I,I:] as Relation of I ;
 dom F = I by PARTFUN1:def_2;
then reconsider f = Sups as Function of I, the carrier of L ;
set X = NetStr(# I,r,f #);
A6: for i, j being Element of NetStr(# I,r,f #) holds i <= j
proof
let i, j be Element of NetStr(# I,r,f #); ::_thesis: i <= j
 [i,j] in the InternalRel of NetStr(# I,r,f #) by ZFMISC_1:87;
hence  i <= j by ORDERS_2:def_5; ::_thesis: verum
end;
A7: NetStr(# I,r,f #) is transitive
proof
let x, y, z be Element of NetStr(# I,r,f #); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z )
assume that
 x <= y and
 y <= z ; ::_thesis: x <= z
thus  x <= z by A6; ::_thesis: verum
end;
 NetStr(# I,r,f #) is directed
proof
let x, y be Element of NetStr(# I,r,f #); :: according to YELLOW_6:def_3 ::_thesis: ex b1 being Element of the carrier of NetStr(# I,r,f #) st
( x <= b1 & y <= b1 )
take  x ; ::_thesis: ( x <= x & y <= x )
thus  ( x <= x & y <= x ) by A6; ::_thesis: verum
end;
then reconsider X = NetStr(# I,r,f #) as strict net of L by A7;
deffunc H1( Element of I) ->  non empty strict NetStr over L = Net-Str ((K . $1),(F . $1));
consider J being ManySortedSet of I such that
A8: for i being Element of I holds J . i = H1(i) from PBOOLE:sch_5();
 for i being set st i in the carrier of X holds
J . i is net of L
proof
let i be set ; ::_thesis: ( i in the carrier of X implies J . i is net of L )
assume  i in the carrier of X ; ::_thesis: J . i is net of L
then reconsider i9 = i as Element of I ;
reconsider rFi = rng (F . i9) as Subset of L ;
A9: rFi is directed by A4;
 J . i9 = Net-Str ((K . i9),(F . i9)) by A8;
hence  J . i is net of L by A9, Th20; ::_thesis: verum
end;
then reconsider J = J as net_set of the carrier of X,L by YELLOW_6:24;
A10: for j being set st j in I holds
ex R being 1-sorted st
( R = J . j & K . j = the carrier of R )
proof
let i be set ; ::_thesis: ( i in I implies ex R being 1-sorted st
( R = J . i & K . i = the carrier of R ) )
assume  i in I ; ::_thesis: ex R being 1-sorted st
( R = J . i & K . i = the carrier of R )
then reconsider i9 = i as Element of I ;
take R = Net-Str ((K . i9),(F . i9)); ::_thesis: ( R = J . i & K . i = the carrier of R )
thus  R = J . i by A8; ::_thesis: K . i = the carrier of R
thus  K . i = the carrier of R by Def10; ::_thesis: verum
end;
A11: doms F = K by YELLOW_7:45
.= Carrier J by A10, PRALG_1:def_13 ;
A12: dom (Frege F) = product (doms F) by PARTFUN1:def_2;
then A13: dom (Infs ) = product (doms F) by FUNCT_2:def_1;
A14: for i being Element of X holds J . i in NetUniv L
proof
let i be Element of X; ::_thesis: J . i in NetUniv L
reconsider i9 = i as Element of I ;
A15: J . i = Net-Str ((K . i9),(F . i9)) by A8;
then reconsider Ji = J . i as strict net of L ;
 K . i9 in the_universe_of the carrier of L by A3;
then  the carrier of Ji in the_universe_of the carrier of L by A15, Def10;
hence  J . i in NetUniv L by YELLOW_6:def_11; ::_thesis: verum
end;
A16: for i being Element of X holds [(J . i),(X . i)] in Scott-Convergence L
proof
let i be Element of X; ::_thesis: [(J . i),(X . i)] in Scott-Convergence L
reconsider i9 = i as Element of I ;
A17: J . i = Net-Str ((K . i9),(F . i9)) by A8;
then reconsider Ji = J . i as reflexive monotone net of L ;
A18: J . i in NetUniv L by A14;
 i in I ;
then  i9 in dom F by PARTFUN1:def_2;
then X . i = Sup by WAYBEL_5:def_1
.= Sup by A17, Def10
.= sup Ji by WAYBEL_2:def_1
.= lim_inf Ji by Th22 ;
then  X . i is_S-limit_of J . i by Def7;
hence  [(J . i),(X . i)] in Scott-Convergence L by A17, A18, Def8; ::_thesis: verum
end;
A19: X in NetUniv L by A2, YELLOW_6:def_11;
then A20: Iterated J in NetUniv L by A14, YELLOW_6:25;
deffunc H2( Element of (Iterated J)) ->  set =  {  ((Iterated J) . p) where p is Element of (Iterated J) : p >= $1  }  ;
 the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26;
then reconsider G = the mapping of (Iterated J) as Function of [: the carrier of X,(product (doms F)):], the carrier of L by A11;
deffunc H3( Element of X, Element of product (doms F)) ->  set =  {  (G . (i,$2)) where i is Element of X : i >= $1  }  ;
defpred S1[ set ] means verum;
deffunc H4( Element of product (doms F)) ->  Element of the carrier of L = "/\" ((rng ((Frege F) . $1)),L);
deffunc H5( Element of X, Element of product (doms F)) ->  Element of the carrier of L = "/\" (H3($1,$2),L);
set D =  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  ;
set D9 =  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  ;
set E9 =  {  H4(g) where g is Element of product (doms F) : S1[g]  }  ;
A21: for i being Element of X
for g being Element of product (doms F) holds H4(g) = H5(i,g)
proof
let j be Element of X; ::_thesis: for g being Element of product (doms F) holds H4(g) = H5(j,g)
let g be Element of product (doms F); ::_thesis: H4(g) = H5(j,g)
 for y being set holds
( y in H3(j,g) iff ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) )
proof
let y be set ; ::_thesis: ( y in H3(j,g) iff ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) )
 g in product (Carrier J) by A11;
then A22: g in the carrier of (product J) by YELLOW_1:def_4;
hereby  ::_thesis: ( ex x being set st
( x in dom ((Frege F) . g) & y = ((Frege F) . g) . x ) implies y in H3(j,g) )
assume  y in H3(j,g) ; ::_thesis: ex x being set st
( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y )
then consider i being Element of X such that
A23: y = G . (i,g) and
 i >= j ;
reconsider x = i as set ;
take x = x; ::_thesis: ( x in dom ((Frege F) . g) & ((Frege F) . g) . x = y )
reconsider i9 = i as Element of I ;
A24: i in I ;
then A25: i9 in dom F by PARTFUN1:def_2;
thus  x in dom ((Frege F) . g) by A24, PARTFUN1:def_2; ::_thesis: ((Frege F) . g) . x = y
thus ((Frege F) . g) . x = (F . i9) . (g . i) by A12, A25, WAYBEL_5:9
.= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10
.= the mapping of (J . i) . (g . i) by A8
.= y by A22, A23, YELLOW_6:def_13 ; ::_thesis: verum
end;
given x being set  such that A26: x in dom ((Frege F) . g) and
A27: y = ((Frege F) . g) . x ; ::_thesis: y in H3(j,g)
A28: x in dom F by A12, A26, WAYBEL_5:8;
reconsider i9 = x as Element of I by A26;
reconsider i = i9 as Element of X ;
A29: i >= j by A6;
y = (F . x) . (g . x) by A12, A27, A28, WAYBEL_5:9
.= the mapping of (Net-Str ((K . i9),(F . i9))) . (g . i) by Def10
.= the mapping of (J . i) . (g . i) by A8
.= G . (i,g) by A22, YELLOW_6:def_13 ;
hence  y in H3(j,g) by A29; ::_thesis: verum
end;
hence  H4(g) = H5(j,g) by FUNCT_1:def_3; ::_thesis: verum
end;
A30:  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  =  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }
proof
A31: the carrier of (Iterated J) = [: the carrier of X,(product (Carrier J)):] by YELLOW_6:26;
A32: for p being Element of (Iterated J)
for i being Element of X
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
proof
let p be Element of (Iterated J); ::_thesis: for i being Element of X
for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
let i be Element of X; ::_thesis: for g being Element of product (doms F) st p = [i,g] holds
"/\" (H2(p),L) = "/\" (H3(i,g),L)
let g be Element of product (doms F); ::_thesis: ( p = [i,g] implies "/\" (H2(p),L) = "/\" (H3(i,g),L) )
assume A33: p = [i,g] ; ::_thesis: "/\" (H2(p),L) = "/\" (H3(i,g),L)
A34: RelStr(# the carrier of (Iterated J), the InternalRel of (Iterated J) #) = RelStr(# the carrier of [:X,(product J):], the InternalRel of [:X,(product J):] #) by YELLOW_6:def_13;
reconsider g9 = g as Element of (product J) by A11, YELLOW_1:def_4;
 g9 in the carrier of (product J) ;
then A35: g9 in product (Carrier J) by YELLOW_1:def_4;
reconsider i9 = i as Element of X ;
 for i being set st i in the carrier of X holds
ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
proof
let i be set ; ::_thesis: ( i in the carrier of X implies ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi ) )
assume  i in the carrier of X ; ::_thesis: ex R being RelStr ex xi, yi being Element of R st
( R = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
then reconsider ii = i as Element of X ;
reconsider i9 = ii as Element of I ;
A36: J . i = Net-Str ((K . i9),(F . i9)) by A8;
set R = Net-Str ((K . i9),(F . i9));
 g9 . ii in the carrier of (Net-Str ((K . i9),(F . i9))) by A36;
then reconsider x = g9 . i as Element of (Net-Str ((K . i9),(F . i9))) ;
take  Net-Str ((K . i9),(F . i9)) ; ::_thesis: ex xi, yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & xi = g9 . i & yi = g9 . i & xi <= yi )
take  x ; ::_thesis: ex yi being Element of (Net-Str ((K . i9),(F . i9))) st
( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & yi = g9 . i & x <= yi )
take  x ; ::_thesis: ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x )
 x <= x ;
hence  ( Net-Str ((K . i9),(F . i9)) = J . i & x = g9 . i & x = g9 . i & x <= x ) by A8; ::_thesis: verum
end;
then A37: g9 <= g9 by A35, YELLOW_1:def_4;
 H3(i,g) c= H2(p)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in H3(i,g) or u in H2(p) )
assume  u in H3(i,g) ; ::_thesis: u in H2(p)
then consider j being Element of X such that
A38: u = the mapping of (Iterated J) . (j,g) and
A39: j >= i ;
reconsider j9 = j as Element of X ;
reconsider q = [j,g] as Element of (Iterated J) by A11, YELLOW_6:26;
 [j9,g9] >= [i9,g9] by A37, A39, YELLOW_3:11;
then A40: q >= p by A33, A34, Lm1;
 u = (Iterated J) . q by A38;
hence  u in H2(p) by A40; ::_thesis: verum
end;
then A41: "/\" (H2(p),L) <= "/\" (H3(i,g),L) by WAYBEL_7:1;
defpred S2[ Element of X] means $1 >= i;
deffunc H6( Element of X) ->  Element of the carrier of L = G . ($1,g);
  {  H6(k) where k is Element of X : S2[k]  }  is Subset of L from DOMAIN_1:sch_8();
then reconsider A = H3(i,g) as Subset of L ;
defpred S3[ Element of (Iterated J)] means $1 >= p;
deffunc H7( Element of (Iterated J)) ->  Element of the carrier of L = (Iterated J) . $1;
  {  H7(z) where z is Element of (Iterated J) : S3[z]  }  is Subset of L from DOMAIN_1:sch_8();
then reconsider B = H2(p) as Subset of L ;
 B is_coarser_than A
proof
let b be Element of L; :: according to YELLOW_4:def_2 ::_thesis: ( not b in B or ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b ) )
assume  b in B ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in A & b1 <= b )
then consider q being Element of (Iterated J) such that
A42: b = (Iterated J) . q and
A43: p <= q ;
consider k being Element of X, f being Element of product (Carrier J) such that
A44: q = [k,f] by A31, DOMAIN_1:1;
reconsider k9 = k as Element of X ;
set a = the mapping of (Iterated J) . (k,g);
 the mapping of (Iterated J) . (k,g) = G . (k,g) ;
then reconsider a = the mapping of (Iterated J) . (k,g) as Element of L ;
take  a ; ::_thesis: ( a in A & a <= b )
reconsider f9 = f as Element of (product J) by YELLOW_1:def_4;
A45: [k9,f9] >= [i9,g9] by A33, A34, A43, A44, Lm1;
then  i <= k by YELLOW_3:11;
hence  a in A ; ::_thesis: a <= b
reconsider k9 = k as Element of I ;
set N = Net-Str ((K . k9),(F . k9));
A46: J . k = Net-Str ((K . k9),(F . k9)) by A8;
reconsider g9k = g9 . k, f9k = f9 . k as Element of (Net-Str ((K . k9),(F . k9))) by A8;
A47: b = (Net-Str ((K . k9),(F . k9))) . f9k by A42, A44, A46, YELLOW_6:27;
reconsider kg = [k,g] as Element of (Iterated J) by A11, YELLOW_6:26;
A48: a = (Iterated J) . kg
.= (Net-Str ((K . k9),(F . k9))) . g9k by A46, YELLOW_6:27 ;
 g9 <= f9 by A45, YELLOW_3:11;
then  g9 . k <= f9 . k by WAYBEL_3:28;
hence  a <= b by A46, A47, A48, Def10; ::_thesis: verum
end;
then  "/\" (H3(i,g),L) <= "/\" (H2(p),L) by Th1;
hence  "/\" (H2(p),L) = "/\" (H3(i,g),L) by A41, YELLOW_0:def_3; ::_thesis: verum
end;
thus   {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  c=  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  c=  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  or e in  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  )
assume  e in  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  ; ::_thesis: e in  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }
then consider p being Element of (Iterated J) such that
A49: e = "/\" (H2(p),L) ;
consider j being Element of X, g being Element of product (doms F) such that
A50: p = [j,g] by A11, A31, DOMAIN_1:1;
 e = "/\" (H3(j,g),L) by A32, A49, A50;
hence  e in  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  or e in  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  )
assume  e in  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  ; ::_thesis: e in  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }
then consider i being Element of X, g being Element of product (doms F) such that
A51: e = "/\" (H3(i,g),L) ;
reconsider j = [i,g] as Element of (Iterated J) by A11, YELLOW_6:26;
 e = "/\" (H2(j),L) by A32, A51;
hence  e in  {  ("/\" (H2(j),L)) where j is Element of (Iterated J) : verum  }  ; ::_thesis: verum
end;
A52:  {  H4(g) where g is Element of product (doms F) : S1[g]  }  =  {  H5(i,g) where i is Element of X, g is Element of product (doms F) : S1[g]  }  from WAYBEL11:sch_1(A21);
 for y being set holds
( y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  iff ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) )
proof
let y be set ; ::_thesis: ( y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  iff ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) )
thus  ( y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  implies ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) ) ::_thesis: ( ex x being set st
( x in dom (Infs ) & y = (Infs ) . x ) implies y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  )
proof
assume  y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  ; ::_thesis: ex x being set st
( x in dom (Infs ) & y = (Infs ) . x )
then consider g being Element of product (doms F) such that
A53: y = "/\" ((rng ((Frege F) . g)),L) ;
take  g ; ::_thesis: ( g in dom (Infs ) & y = (Infs ) . g )
thus A54: g in dom (Infs ) by A13; ::_thesis: y = (Infs ) . g
thus y = //\ (((Frege F) . g),L) by A53, YELLOW_2:def_6
.= (Infs ) . g by A54, WAYBEL_5:def_2 ; ::_thesis: verum
end;
given x being set  such that A55: x in dom (Infs ) and
A56: y = (Infs ) . x ; ::_thesis: y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }
reconsider x = x as Element of product (doms F) by A55, PARTFUN1:def_2;
y = //\ (((Frege F) . x),L) by A55, A56, WAYBEL_5:def_2
.= "/\" ((rng ((Frege F) . x)),L) by YELLOW_2:def_6 ;
hence  y in  {  H4(g) where g is Element of product (doms F) : S1[g]  }  ; ::_thesis: verum
end;
then  rng (Infs ) =  {  H4(g) where g is Element of product (doms F) : S1[g]  }  by FUNCT_1:def_3;
then A57: Sup = lim_inf (Iterated J) by A30, A52, YELLOW_2:def_5;
reconsider x9 = Inf as Element of L ;
set X1 =  {  (Inf ) where j9 is Element of X : verum  }  ;
set X2 =  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  ;
A58:  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  =  {  (Inf ) where j9 is Element of X : verum  }
proof
A59: for j being Element of X holds Inf = "/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)
proof
let j be Element of X; ::_thesis: Inf = "/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)
set X3 =  {  (X . i) where i is Element of X : i >= j  }  ;
 for e being set holds
( e in  {  (X . i) where i is Element of X : i >= j  }  iff ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) )
proof
let e be set ; ::_thesis: ( e in  {  (X . i) where i is Element of X : i >= j  }  iff ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) )
hereby  ::_thesis: ( ex u being set st
( u in dom (Sups ) & e = (Sups ) . u ) implies e in  {  (X . i) where i is Element of X : i >= j  }  )
assume  e in  {  (X . i) where i is Element of X : i >= j  }  ; ::_thesis: ex u being set st
( u in dom (Sups ) & e = (Sups ) . u )
then consider i being Element of X such that
A60: e = X . i and
 i >= j ;
reconsider u = i as set ;
take u = u; ::_thesis: ( u in dom (Sups ) & e = (Sups ) . u )
 u in I ;
hence  u in dom (Sups ) by FUNCT_2:def_1; ::_thesis: e = (Sups ) . u
thus  e = (Sups ) . u by A60; ::_thesis: verum
end;
given u being set  such that A61: u in dom (Sups ) and
A62: e = (Sups ) . u ; ::_thesis: e in  {  (X . i) where i is Element of X : i >= j  }
reconsider i = u as Element of X by A61, FUNCT_2:def_1;
A63: i >= j by A6;
 e = X . i by A62;
hence  e in  {  (X . i) where i is Element of X : i >= j  }  by A63; ::_thesis: verum
end;
then  rng (Sups ) =  {  (X . i) where i is Element of X : i >= j  }  by FUNCT_1:def_3;
hence  Inf = "/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L) by YELLOW_2:def_6; ::_thesis: verum
end;
thus   {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  c=  {  (Inf ) where j9 is Element of X : verum  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (Inf ) where j9 is Element of X : verum  }  c=  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  or u in  {  (Inf ) where j9 is Element of X : verum  }  )
assume  u in  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  ; ::_thesis: u in  {  (Inf ) where j9 is Element of X : verum  }
then  ex j being Element of X st u = "/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L) ;
then  u = Inf by A59;
hence  u in  {  (Inf ) where j9 is Element of X : verum  }  ; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in  {  (Inf ) where j9 is Element of X : verum  }  or u in  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  )
set j = the Element of X;
assume  u in  {  (Inf ) where j9 is Element of X : verum  }  ; ::_thesis: u in  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }
then  ex j being Element of X st u = Inf ;
then  u = "/\" ( {  (X . i) where i is Element of X : i >= the Element of X  }  ,L) by A59;
hence  u in  {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  ; ::_thesis: verum
end;
now__::_thesis:_for_u_being_set_holds_
(_u_in__{__(Inf_)_where_j9_is_Element_of_X_:_verum__}__iff_u_in_{(Inf_)}_)
let u be set ; ::_thesis: ( u in  {  (Inf ) where j9 is Element of X : verum  }  iff u in {(Inf )} )
 ( u in  {  (Inf ) where j9 is Element of X : verum  }  iff ex j9 being Element of X st u = Inf ) ;
then  ( u in  {  (Inf ) where j9 is Element of X : verum  }  iff u = Inf ) ;
hence  ( u in  {  (Inf ) where j9 is Element of X : verum  }  iff u in {(Inf )} ) by TARSKI:def_1; ::_thesis: verum
end;
then  "\/" ( {  ("/\" ( {  (X . i) where i is Element of X : i >= j  }  ,L)) where j is Element of X : verum  }  ,L) = sup {x9} by A58, TARSKI:1
.= Inf by YELLOW_0:39 ;
then  Inf <= lim_inf X ;
then  Inf is_S-limit_of X by Def7;
then  [X,(Inf )] in Scott-Convergence L by A19, Def8;
then  [(Iterated J),(Inf )] in Scott-Convergence L by A1, A16, YELLOW_6:def_23;
then  Inf is_S-limit_of Iterated J by A20, Def8;
then  Inf <= Sup by A57, Def7;
hence  Inf = Sup by A5, ORDERS_2:2; ::_thesis: verum
end;
hence  L is continuous by WAYBEL_5:18; ::_thesis: verum
end;

theorem :: WAYBEL11:40
for T being complete Scott TopLattice holds
( T is continuous iff Convergence T = Scott-Convergence T )
proof
let T be complete Scott TopLattice; ::_thesis: ( T is continuous iff Convergence T = Scott-Convergence T )
hereby  ::_thesis: ( Convergence T = Scott-Convergence T implies T is continuous )
assume  T is continuous ; ::_thesis: Convergence T = Scott-Convergence T
then reconsider L = T as complete continuous Scott TopLattice ;
 TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence T) by Th32;
hence  Convergence T = Convergence (ConvergenceSpace (Scott-Convergence L)) by Lm8
.= Scott-Convergence T by YELLOW_6:44 ;
::_thesis: verum
end;
thus  ( Convergence T = Scott-Convergence T implies T is continuous ) by Th39; ::_thesis: verum
end;

theorem Th41: :: WAYBEL11:41
for T being complete Scott TopLattice
for S being upper Subset of T st S is Open holds
S is open
proof
let T be complete Scott TopLattice; ::_thesis: for S being upper Subset of T st S is Open holds
S is open
let S be upper Subset of T; ::_thesis: ( S is Open implies S is open )
assume A1: for x being Element of T st x in S holds
ex y being Element of T st
( y in S & y << x ) ; :: according to WAYBEL_6:def_1 ::_thesis: S is open
 S is inaccessible
proof
let D be non empty directed Subset of T; :: according to WAYBEL11:def_1 ::_thesis: ( sup D in S implies D meets S )
assume  sup D in S ; ::_thesis: D meets S
then consider y being Element of T such that
A2: y in S and
A3: y << sup D by A1;
consider d being Element of T such that
A4: d in D and
A5: y <= d by A3, WAYBEL_3:def_1;
 d in S by A2, A5, WAYBEL_0:def_20;
hence  D meets S by A4, XBOOLE_0:3; ::_thesis: verum
end;
hence  S is open by Def4; ::_thesis: verum
end;

theorem Th42: :: WAYBEL11:42
for L being non empty RelStr
for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
proof
let L be non empty RelStr ; ::_thesis: for S being upper Subset of L
for x being Element of L st x in S holds
uparrow x c= S
let S be upper Subset of L; ::_thesis: for x being Element of L st x in S holds
uparrow x c= S
let x be Element of L; ::_thesis: ( x in S implies uparrow x c= S )
assume A1: x in S ; ::_thesis: uparrow x c= S
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in uparrow x or e in S )
assume A2: e in uparrow x ; ::_thesis: e in S
then reconsider y = e as Element of L ;
 x <= y by A2, WAYBEL_0:18;
hence  e in S by A1, WAYBEL_0:def_20; ::_thesis: verum
end;

theorem Th43: :: WAYBEL11:43
for L being complete continuous Scott TopLattice
for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
proof
let L be complete continuous Scott TopLattice; ::_thesis: for p being Element of L
for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let p be Element of L; ::_thesis: for S being Subset of L st S is open & p in S holds
ex q being Element of L st
( q << p & q in S )
let S be Subset of L; ::_thesis: ( S is open & p in S implies ex q being Element of L st
( q << p & q in S ) )
assume that
A1: S is open and
A2: p in S ; ::_thesis: ex q being Element of L st
( q << p & q in S )
A3: S is inaccessible by A1, Def4;
 sup (waybelow p) = p by WAYBEL_3:def_5;
then  waybelow p meets S by A2, A3, Def1;
then  (waybelow p) /\ S <> {} by XBOOLE_0:def_7;
then consider u being Element of L such that
A4: u in (waybelow p) /\ S by SUBSET_1:4;
reconsider u = u as Element of L ;
take  u ; ::_thesis: ( u << p & u in S )
 u in waybelow p by A4, XBOOLE_0:def_4;
hence  u << p by WAYBEL_3:7; ::_thesis: u in S
thus  u in S by A4, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th44: :: WAYBEL11:44
for L being complete continuous Scott TopLattice
for p being Element of L holds  {  (wayabove q) where q is Element of L : q << p  }  is Basis of
proof
let L be complete continuous Scott TopLattice; ::_thesis: for p being Element of L holds  {  (wayabove q) where q is Element of L : q << p  }  is Basis of
let p be Element of L; ::_thesis:  {  (wayabove q) where q is Element of L : q << p  }  is Basis of
set X =  {  (wayabove q) where q is Element of L : q << p  }  ;
  {  (wayabove q) where q is Element of L : q << p  }  c= bool the carrier of L
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (wayabove q) where q is Element of L : q << p  }  or e in bool the carrier of L )
assume  e in  {  (wayabove q) where q is Element of L : q << p  }  ; ::_thesis: e in bool the carrier of L
then  ex q being Element of L st
( e = wayabove q & q << p ) ;
hence  e in bool the carrier of L ; ::_thesis: verum
end;
then reconsider X =  {  (wayabove q) where q is Element of L : q << p  }  as Subset-Family of L ;
 X is Basis of
proof
A1: X is open
proof
let e be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not e in X or e is open )
assume  e in X ; ::_thesis: e is open
then consider q being Element of L such that
A2: e = wayabove q and
 q << p ;
 wayabove q is open by Th36;
hence  e is open by A2; ::_thesis: verum
end;
 X is p -quasi_basis
proof
 for Y being set st Y in X holds
p in Y
proof
let e be set ; ::_thesis: ( e in X implies p in e )
assume  e in X ; ::_thesis: p in e
then  ex q being Element of L st
( e = wayabove q & q << p ) ;
hence  p in e ; ::_thesis: verum
end;
hence  p in Intersect X by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not p in b1 or ex b2 being Element of bool the carrier of L st
( b2 in X & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not p in S or ex b1 being Element of bool the carrier of L st
( b1 in X & b1 c= S ) )
assume that
A3: S is open and
A4: p in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in X & b1 c= S )
consider u being Element of L such that
A5: u << p and
A6: u in S by A3, A4, Th43;
take V = wayabove u; ::_thesis: ( V in X & V c= S )
thus  V in X by A5; ::_thesis: V c= S
A7: S is upper by A3, Def4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
 uparrow u c= S by A6, A7, Th42;
hence  V c= S by A8, XBOOLE_1:1; ::_thesis: verum
end;
hence  X is Basis of by A1; ::_thesis: verum
end;
hence   {  (wayabove q) where q is Element of L : q << p  }  is Basis of ; ::_thesis: verum
end;

theorem Th45: :: WAYBEL11:45
for T being complete continuous Scott TopLattice holds  {  (wayabove x) where x is Element of T : verum  }  is Basis of T
proof
let T be complete continuous Scott TopLattice; ::_thesis:  {  (wayabove x) where x is Element of T : verum  }  is Basis of T
set B =  {  (wayabove x) where x is Element of T : verum  }  ;
A1:  {  (wayabove x) where x is Element of T : verum  }  c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (wayabove x) where x is Element of T : verum  }  or e in the topology of T )
assume  e in  {  (wayabove x) where x is Element of T : verum  }  ; ::_thesis: e in the topology of T
then consider x being Element of T such that
A2: e = wayabove x ;
 wayabove x is open by Th36;
hence  e in the topology of T by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider P =  {  (wayabove x) where x is Element of T : verum  }  as Subset-Family of T by XBOOLE_1:1;
 for x being Point of T ex B being Basis of st B c= P
proof
let x be Point of T; ::_thesis: ex B being Basis of st B c= P
reconsider p = x as Element of T ;
reconsider A =  {  (wayabove q) where q is Element of T : q << p  }  as Basis of by Th44;
take  A ; ::_thesis: A c= P
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in A or u in P )
assume  u in A ; ::_thesis: u in P
then  ex q being Element of T st
( u = wayabove q & q << p ) ;
hence  u in P ; ::_thesis: verum
end;
hence   {  (wayabove x) where x is Element of T : verum  }  is Basis of T by A1, YELLOW_8:14; ::_thesis: verum
end;

theorem :: WAYBEL11:46
for T being complete continuous Scott TopLattice
for S being upper Subset of T holds
( S is open iff S is Open )
proof
let T be complete continuous Scott TopLattice; ::_thesis: for S being upper Subset of T holds
( S is open iff S is Open )
let S be upper Subset of T; ::_thesis: ( S is open iff S is Open )
thus  ( S is open implies S is Open ) ::_thesis: ( S is Open implies S is open )
proof
assume A1: S is open ; ::_thesis: S is Open
let x be Element of T; :: according to WAYBEL_6:def_1 ::_thesis: ( not x in S or ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) )
assume  x in S ; ::_thesis: ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x )
then  ex y being Element of T st
( y << x & y in S ) by A1, Th43;
hence  ex b1 being Element of the carrier of T st
( b1 in S & b1 is_way_below x ) ; ::_thesis: verum
end;
thus  ( S is Open implies S is open ) by Th41; ::_thesis: verum
end;

theorem :: WAYBEL11:47
for T being complete continuous Scott TopLattice
for p being Element of T holds Int (uparrow p) = wayabove p
proof
let T be complete continuous Scott TopLattice; ::_thesis: for p being Element of T holds Int (uparrow p) = wayabove p
let p be Element of T; ::_thesis: Int (uparrow p) = wayabove p
thus  Int (uparrow p) c= wayabove p :: according to XBOOLE_0:def_10 ::_thesis: wayabove p c= Int (uparrow p)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Int (uparrow p) or y in wayabove p )
assume A1: y in Int (uparrow p) ; ::_thesis: y in wayabove p
then reconsider q = y as Element of T ;
reconsider S = Int (uparrow p) as Subset of T ;
consider u being Element of T such that
A2: u << q and
A3: u in S by A1, Th43;
 S c= uparrow p by TOPS_1:16;
then  p <= u by A3, WAYBEL_0:18;
then  p << q by A2, WAYBEL_3:2;
hence  y in wayabove p ; ::_thesis: verum
end;
 wayabove p c= uparrow p by WAYBEL_3:11;
hence  wayabove p c= Int (uparrow p) by Th36, TOPS_1:24; ::_thesis: verum
end;

theorem :: WAYBEL11:48
for T being complete continuous Scott TopLattice
for S being Subset of T holds Int S = union  {  (wayabove x) where x is Element of T : wayabove x c= S  }
proof
let T be complete continuous Scott TopLattice; ::_thesis: for S being Subset of T holds Int S = union  {  (wayabove x) where x is Element of T : wayabove x c= S  }
let S be Subset of T; ::_thesis: Int S = union  {  (wayabove x) where x is Element of T : wayabove x c= S  }
set B =  {  (wayabove x) where x is Element of T : verum  }  ;
set I =  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  ;
set P =  {  (wayabove x) where x is Element of T : wayabove x c= S  }  ;
A1:  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  =  {  (wayabove x) where x is Element of T : wayabove x c= S  }
proof
thus   {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  c=  {  (wayabove x) where x is Element of T : wayabove x c= S  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (wayabove x) where x is Element of T : wayabove x c= S  }  c=  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  or e in  {  (wayabove x) where x is Element of T : wayabove x c= S  }  )
assume  e in  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  ; ::_thesis: e in  {  (wayabove x) where x is Element of T : wayabove x c= S  }
then consider G being Subset of T such that
A2: e = G and
A3: G in  {  (wayabove x) where x is Element of T : verum  }  and
A4: G c= S ;
 ex x being Element of T st G = wayabove x by A3;
hence  e in  {  (wayabove x) where x is Element of T : wayabove x c= S  }  by A2, A4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in  {  (wayabove x) where x is Element of T : wayabove x c= S  }  or e in  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  )
assume  e in  {  (wayabove x) where x is Element of T : wayabove x c= S  }  ; ::_thesis: e in  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }
then consider x being Element of T such that
A5: e = wayabove x and
A6: wayabove x c= S ;
 wayabove x in  {  (wayabove x) where x is Element of T : verum  }  ;
hence  e in  {  G where G is Subset of T : ( G in  {  (wayabove x) where x is Element of T : verum  }  & G c= S )  }  by A5, A6; ::_thesis: verum
end;
  {  (wayabove x) where x is Element of T : verum  }  is Basis of T by Th45;
hence  Int S = union  {  (wayabove x) where x is Element of T : wayabove x c= S  }  by A1, YELLOW_8:11; ::_thesis: verum
end;