:: WAYBEL14 semantic presentation

begin

theorem Th1: :: WAYBEL14:1
for X being set
for F being finite Subset-Family of X ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
proof
let X be set ; ::_thesis: for F being finite Subset-Family of X ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
defpred S1[ Nat] means  for F being finite Subset-Family of X st card F = $1 holds
ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) );
A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_
S1[n_+_1]
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
thus  S1[n + 1] ::_thesis: verum
proof
let F be finite Subset-Family of X; ::_thesis: ( card F = n + 1 implies ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) )
assume A3: card F = n + 1 ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
percases ( ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) or for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ) ;
suppose ex g being Subset of X st
( g in F & g c= union (F \ {g}) ) ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
then consider g being Subset of X such that
A4: g in F and
A5: g c= union (F \ {g}) ;
reconsider FF = F \ {g} as finite Subset-Family of X ;
 {g} c= F by A4, ZFMISC_1:31;
then A6: F = FF \/ {g} by XBOOLE_1:45;
A7: union F c= union FF
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in union FF )
assume  x in union F ; ::_thesis: x in union FF
then consider X being set  such that
A8: x in X and
A9: X in F by TARSKI:def_4;
percases ( X in FF or X in {g} ) by A6, A9, XBOOLE_0:def_3;
suppose X in FF ; ::_thesis: x in union FF
then  X c= union FF by ZFMISC_1:74;
hence  x in union FF by A8; ::_thesis: verum
end;
suppose X in {g} ; ::_thesis: x in union FF
then  X = g by TARSKI:def_1;
hence  x in union FF by A5, A8; ::_thesis: verum
end;
end;
end;
 g in {g} by TARSKI:def_1;
then  not g in FF by XBOOLE_0:def_5;
then  card (FF \/ {g}) = (card FF) + 1 by CARD_2:41;
then consider G being finite Subset-Family of X such that
A10: G c= FF and
A11: union G = union FF and
A12: for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A2, A3, A6, XCMPLX_1:2;
take  G ; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
 FF c= F by A6, XBOOLE_1:7;
hence  G c= F by A10, XBOOLE_1:1; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
 union FF c= union F by A6, XBOOLE_1:7, ZFMISC_1:77;
hence  union G = union F by A11, A7, XBOOLE_0:def_10; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus  for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A12; ::_thesis: verum
end;
supposeA13: for g being Subset of X holds
( not g in F or not g c= union (F \ {g}) ) ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
take G = F; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus  G c= F ; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus  union G = union F ; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus  for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A13; ::_thesis: verum
end;
end;
end;
end;
let F be finite Subset-Family of X; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
A14: card F = card F ;
A15: S1[ 0 ]
proof
let F be finite Subset-Family of X; ::_thesis: ( card F = 0 implies ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) )
assume A16: card F = 0 ; ::_thesis: ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
take G = F; ::_thesis: ( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus  G c= F ; ::_thesis: ( union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) )
thus  union G = union F ; ::_thesis: for g being Subset of X st g in G holds
not g c= union (G \ {g})
thus  for g being Subset of X st g in G holds
not g c= union (G \ {g}) by A16; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A15, A1);
hence  ex G being finite Subset-Family of X st
( G c= F & union G = union F & ( for g being Subset of X st g in G holds
not g c= union (G \ {g}) ) ) by A14; ::_thesis: verum
end;

Lm1:  for S being 1-sorted
for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
proof
let S be 1-sorted ; ::_thesis: for X, Y being Subset of S holds
( X c= Y ` iff Y c= X ` )
let X, Y be Subset of S; ::_thesis: ( X c= Y ` iff Y c= X ` )
 Y = (Y `) ` ;
hence  ( X c= Y ` iff Y c= X ` ) by SUBSET_1:12; ::_thesis: verum
end;

theorem Th2: :: WAYBEL14:2
for S being 1-sorted
for X being Subset of S holds
( X ` = the carrier of S iff X is empty )
proof
let S be 1-sorted ; ::_thesis: for X being Subset of S holds
( X ` = the carrier of S iff X is empty )
let X be Subset of S; ::_thesis: ( X ` = the carrier of S iff X is empty )
hereby  ::_thesis: ( X is empty implies X ` = the carrier of S )
assume  X ` = the carrier of S ; ::_thesis: X is empty
then  X = ([#] the carrier of S) ` ;
hence  X is empty by XBOOLE_1:37; ::_thesis: verum
end;
assume  X is empty ; ::_thesis: X ` = the carrier of S
hence  X ` = the carrier of S ; ::_thesis: verum
end;

theorem Th3: :: WAYBEL14:3
for R being non empty transitive antisymmetric with_infima RelStr
for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
proof
let R be non empty transitive antisymmetric with_infima RelStr ; ::_thesis: for x, y being Element of R holds downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
let x, y be Element of R; ::_thesis: downarrow (x "/\" y) = (downarrow x) /\ (downarrow y)
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_downarrow_(x_"/\"_y)_implies_z_in_(downarrow_x)_/\_(downarrow_y)_)_&_(_z_in_(downarrow_x)_/\_(downarrow_y)_implies_z_in_downarrow_(x_"/\"_y)_)_)
let z be set ; ::_thesis: ( ( z in downarrow (x "/\" y) implies z in (downarrow x) /\ (downarrow y) ) & ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) ) )
hereby  ::_thesis: ( z in (downarrow x) /\ (downarrow y) implies z in downarrow (x "/\" y) )
assume A1: z in downarrow (x "/\" y) ; ::_thesis: z in (downarrow x) /\ (downarrow y)
then reconsider z9 = z as Element of R ;
A2: z9 <= x "/\" y by A1, WAYBEL_0:17;
 x "/\" y <= y by YELLOW_0:23;
then  z9 <= y by A2, YELLOW_0:def_2;
then A3: z9 in downarrow y by WAYBEL_0:17;
 x "/\" y <= x by YELLOW_0:23;
then  z9 <= x by A2, YELLOW_0:def_2;
then  z9 in downarrow x by WAYBEL_0:17;
hence  z in (downarrow x) /\ (downarrow y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: z in (downarrow x) /\ (downarrow y) ; ::_thesis: z in downarrow (x "/\" y)
then reconsider z9 = z as Element of R ;
 z in downarrow y by A4, XBOOLE_0:def_4;
then A5: z9 <= y by WAYBEL_0:17;
 z in downarrow x by A4, XBOOLE_0:def_4;
then  z9 <= x by WAYBEL_0:17;
then  x "/\" y >= z9 by A5, YELLOW_0:23;
hence  z in downarrow (x "/\" y) by WAYBEL_0:17; ::_thesis: verum
end;
hence  downarrow (x "/\" y) = (downarrow x) /\ (downarrow y) by TARSKI:1; ::_thesis: verum
end;

theorem :: WAYBEL14:4
for R being non empty transitive antisymmetric with_suprema RelStr
for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
proof
let R be non empty transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y being Element of R holds uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
let x, y be Element of R; ::_thesis: uparrow (x "\/" y) = (uparrow x) /\ (uparrow y)
now__::_thesis:_for_z_being_set_holds_
(_(_z_in_uparrow_(x_"\/"_y)_implies_z_in_(uparrow_x)_/\_(uparrow_y)_)_&_(_z_in_(uparrow_x)_/\_(uparrow_y)_implies_z_in_uparrow_(x_"\/"_y)_)_)
let z be set ; ::_thesis: ( ( z in uparrow (x "\/" y) implies z in (uparrow x) /\ (uparrow y) ) & ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) ) )
hereby  ::_thesis: ( z in (uparrow x) /\ (uparrow y) implies z in uparrow (x "\/" y) )
assume A1: z in uparrow (x "\/" y) ; ::_thesis: z in (uparrow x) /\ (uparrow y)
then reconsider z9 = z as Element of R ;
A2: z9 >= x "\/" y by A1, WAYBEL_0:18;
 x "\/" y >= y by YELLOW_0:22;
then  z9 >= y by A2, YELLOW_0:def_2;
then A3: z9 in uparrow y by WAYBEL_0:18;
 x "\/" y >= x by YELLOW_0:22;
then  z9 >= x by A2, YELLOW_0:def_2;
then  z9 in uparrow x by WAYBEL_0:18;
hence  z in (uparrow x) /\ (uparrow y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A4: z in (uparrow x) /\ (uparrow y) ; ::_thesis: z in uparrow (x "\/" y)
then reconsider z9 = z as Element of R ;
 z in uparrow y by A4, XBOOLE_0:def_4;
then A5: z9 >= y by WAYBEL_0:18;
 z in uparrow x by A4, XBOOLE_0:def_4;
then  z9 >= x by WAYBEL_0:18;
then  x "\/" y <= z9 by A5, YELLOW_0:22;
hence  z in uparrow (x "\/" y) by WAYBEL_0:18; ::_thesis: verum
end;
hence  uparrow (x "\/" y) = (uparrow x) /\ (uparrow y) by TARSKI:1; ::_thesis: verum
end;

theorem Th5: :: WAYBEL14:5
for L being non empty antisymmetric complete RelStr
for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)
proof
let L be non empty antisymmetric complete RelStr ; ::_thesis: for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)
let X be lower Subset of L; ::_thesis: ( sup X in X implies X = downarrow (sup X) )
assume A1: sup X in X ; ::_thesis: X = downarrow (sup X)
 X is_<=_than sup X by YELLOW_0:32;
hence  X c= downarrow (sup X) by YELLOW_2:1; :: according to XBOOLE_0:def_10 ::_thesis: downarrow (sup X) c= X
thus  downarrow (sup X) c= X by A1, WAYBEL11:6; ::_thesis: verum
end;

theorem :: WAYBEL14:6
for L being non empty antisymmetric complete RelStr
for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)
proof
let L be non empty antisymmetric complete RelStr ; ::_thesis: for X being upper Subset of L st inf X in X holds
X = uparrow (inf X)
let X be upper Subset of L; ::_thesis: ( inf X in X implies X = uparrow (inf X) )
assume A1: inf X in X ; ::_thesis: X = uparrow (inf X)
 X is_>=_than inf X by YELLOW_0:33;
hence  X c= uparrow (inf X) by YELLOW_2:2; :: according to XBOOLE_0:def_10 ::_thesis: uparrow (inf X) c= X
thus  uparrow (inf X) c= X by A1, WAYBEL11:42; ::_thesis: verum
end;

theorem Th7: :: WAYBEL14:7
for R being non empty reflexive transitive RelStr
for x, y being Element of R holds
( x << y iff uparrow y c= wayabove x )
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of R holds
( x << y iff uparrow y c= wayabove x )
let x, y be Element of R; ::_thesis: ( x << y iff uparrow y c= wayabove x )
hereby  ::_thesis: ( uparrow y c= wayabove x implies x << y )
assume A1: x << y ; ::_thesis: uparrow y c= wayabove x
thus  uparrow y c= wayabove x ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in uparrow y or z in wayabove x )
assume A2: z in uparrow y ; ::_thesis: z in wayabove x
then reconsider z9 = z as Element of R ;
 y <= z9 by A2, WAYBEL_0:18;
then  x << z9 by A1, WAYBEL_3:2;
hence  z in wayabove x ; ::_thesis: verum
end;
end;
 y <= y ;
then A3: y in uparrow y by WAYBEL_0:18;
assume  uparrow y c= wayabove x ; ::_thesis: x << y
hence  x << y by A3, WAYBEL_3:8; ::_thesis: verum
end;

theorem :: WAYBEL14:8
for R being non empty reflexive transitive RelStr
for x, y being Element of R holds
( x << y iff downarrow x c= waybelow y )
proof
let R be non empty reflexive transitive RelStr ; ::_thesis: for x, y being Element of R holds
( x << y iff downarrow x c= waybelow y )
let x, y be Element of R; ::_thesis: ( x << y iff downarrow x c= waybelow y )
hereby  ::_thesis: ( downarrow x c= waybelow y implies x << y )
assume A1: x << y ; ::_thesis: downarrow x c= waybelow y
thus  downarrow x c= waybelow y ::_thesis: verum
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in downarrow x or z in waybelow y )
assume A2: z in downarrow x ; ::_thesis: z in waybelow y
then reconsider z9 = z as Element of R ;
 z9 <= x by A2, WAYBEL_0:17;
then  z9 << y by A1, WAYBEL_3:2;
hence  z in waybelow y ; ::_thesis: verum
end;
end;
 x <= x ;
then A3: x in downarrow x by WAYBEL_0:17;
assume  downarrow x c= waybelow y ; ::_thesis: x << y
hence  x << y by A3, WAYBEL_3:7; ::_thesis: verum
end;

theorem Th9: :: WAYBEL14:9
for R being non empty reflexive antisymmetric complete RelStr
for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )
proof
let R be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for x being Element of R holds
( sup (waybelow x) <= x & x <= inf (wayabove x) )
let x be Element of R; ::_thesis: ( sup (waybelow x) <= x & x <= inf (wayabove x) )
 x is_>=_than waybelow x by WAYBEL_3:9;
hence  sup (waybelow x) <= x by YELLOW_0:32; ::_thesis: x <= inf (wayabove x)
 x is_<=_than wayabove x by WAYBEL_3:10;
hence  x <= inf (wayabove x) by YELLOW_0:33; ::_thesis: verum
end;

theorem Th10: :: WAYBEL14:10
for L being non empty antisymmetric lower-bounded RelStr holds uparrow (Bottom L) = the carrier of L
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: uparrow (Bottom L) = the carrier of L
set uL = uparrow (Bottom L);
set cL = the carrier of L;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_uparrow_(Bottom_L)_implies_x_in_the_carrier_of_L_)_&_(_x_in_the_carrier_of_L_implies_x_in_uparrow_(Bottom_L)_)_)
let x be set ; ::_thesis: ( ( x in uparrow (Bottom L) implies x in the carrier of L ) & ( x in the carrier of L implies x in uparrow (Bottom L) ) )
thus  ( x in uparrow (Bottom L) implies x in the carrier of L ) ; ::_thesis: ( x in the carrier of L implies x in uparrow (Bottom L) )
assume  x in the carrier of L ; ::_thesis: x in uparrow (Bottom L)
then reconsider x9 = x as Element of L ;
 Bottom L <= x9 by YELLOW_0:44;
hence  x in uparrow (Bottom L) by WAYBEL_0:18; ::_thesis: verum
end;
hence  uparrow (Bottom L) = the carrier of L by TARSKI:1; ::_thesis: verum
end;

theorem :: WAYBEL14:11
for L being non empty antisymmetric upper-bounded RelStr holds downarrow (Top L) = the carrier of L
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: downarrow (Top L) = the carrier of L
set uL = downarrow (Top L);
set cL = the carrier of L;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_downarrow_(Top_L)_implies_x_in_the_carrier_of_L_)_&_(_x_in_the_carrier_of_L_implies_x_in_downarrow_(Top_L)_)_)
let x be set ; ::_thesis: ( ( x in downarrow (Top L) implies x in the carrier of L ) & ( x in the carrier of L implies x in downarrow (Top L) ) )
thus  ( x in downarrow (Top L) implies x in the carrier of L ) ; ::_thesis: ( x in the carrier of L implies x in downarrow (Top L) )
assume  x in the carrier of L ; ::_thesis: x in downarrow (Top L)
then reconsider x9 = x as Element of L ;
 Top L >= x9 by YELLOW_0:45;
hence  x in downarrow (Top L) by WAYBEL_0:17; ::_thesis: verum
end;
hence  downarrow (Top L) = the carrier of L by TARSKI:1; ::_thesis: verum
end;

theorem Th12: :: WAYBEL14:12
for P being with_suprema Poset
for x, y being Element of P holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
proof
let R be with_suprema Poset; ::_thesis: for x, y being Element of R holds (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
let x, y be Element of R; ::_thesis: (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y)
 ( {x} "\/" {y} = {(x "\/" y)} & (uparrow x) "\/" (uparrow y) c= uparrow ((uparrow x) "\/" (uparrow y)) ) by WAYBEL_0:16, YELLOW_4:19;
then A1: (uparrow x) "\/" (uparrow y) c= uparrow (x "\/" y) by YELLOW_4:35;
 ( wayabove x c= uparrow x & wayabove y c= uparrow y ) by WAYBEL_3:11;
then  (wayabove x) "\/" (wayabove y) c= (uparrow x) "\/" (uparrow y) by YELLOW_4:21;
hence  (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: WAYBEL14:13
for P being with_infima Poset
for x, y being Element of P holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
proof
let R be with_infima Poset; ::_thesis: for x, y being Element of R holds (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
let x, y be Element of R; ::_thesis: (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y)
 ( {x} "/\" {y} = {(x "/\" y)} & (downarrow x) "/\" (downarrow y) c= downarrow ((downarrow x) "/\" (downarrow y)) ) by WAYBEL_0:16, YELLOW_4:46;
then A1: (downarrow x) "/\" (downarrow y) c= downarrow (x "/\" y) by YELLOW_4:62;
 ( waybelow x c= downarrow x & waybelow y c= downarrow y ) by WAYBEL_3:11;
then  (waybelow x) "/\" (waybelow y) c= (downarrow x) "/\" (downarrow y) by YELLOW_4:48;
hence  (waybelow x) "/\" (waybelow y) c= downarrow (x "/\" y) by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th14: :: WAYBEL14:14
for R being non empty with_suprema Poset
for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
proof
let R be non empty with_suprema Poset; ::_thesis: for l being Element of R holds
( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
let l be Element of R; ::_thesis: ( l is co-prime iff for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) )
hereby  ::_thesis: ( ( for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ) implies l is co-prime )
assume  l is co-prime ; ::_thesis: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y )
then A1: l ~ is prime by WAYBEL_6:def_8;
let x, y be Element of R; ::_thesis: ( not l <= x "\/" y or l <= x or l <= y )
assume  l <= x "\/" y ; ::_thesis: ( l <= x or l <= y )
then A2: (x "\/" y) ~ <= l ~ by LATTICE3:9;
(x "\/" y) ~ = x "\/" y by LATTICE3:def_6
.= (x ~) "/\" (y ~) by YELLOW_7:23 ;
then  ( x ~ <= l ~ or y ~ <= l ~ ) by A1, A2, WAYBEL_6:def_6;
hence  ( l <= x or l <= y ) by LATTICE3:9; ::_thesis: verum
end;
assume A3: for x, y being Element of R holds
( not l <= x "\/" y or l <= x or l <= y ) ; ::_thesis: l is co-prime
let x, y be Element of (R ~); :: according to WAYBEL_6:def_6,WAYBEL_6:def_8 ::_thesis: ( not x "/\" y <= l ~ or x <= l ~ or y <= l ~ )
A4: ~ (x "/\" y) = x "/\" y by LATTICE3:def_7
.= (~ x) "\/" (~ y) by YELLOW_7:24 ;
assume  x "/\" y <= l ~ ; ::_thesis: ( x <= l ~ or y <= l ~ )
then  l <= (~ x) "\/" (~ y) by A4, YELLOW_7:2;
then  ( l <= ~ x or l <= ~ y ) by A3;
hence  ( x <= l ~ or y <= l ~ ) by YELLOW_7:2; ::_thesis: verum
end;

theorem Th15: :: WAYBEL14:15
for P being non empty complete Poset
for V being non empty Subset of P holds downarrow (inf V) = meet  {  (downarrow u) where u is Element of P : u in V  }
proof
let P be non empty complete Poset; ::_thesis: for V being non empty Subset of P holds downarrow (inf V) = meet  {  (downarrow u) where u is Element of P : u in V  }
let V be non empty Subset of P; ::_thesis: downarrow (inf V) = meet  {  (downarrow u) where u is Element of P : u in V  }
set F =  {  (downarrow u) where u is Element of P : u in V  }  ;
consider u being set  such that
A1: u in V by XBOOLE_0:def_1;
A2:  {  (downarrow u) where u is Element of P : u in V  }  c= bool the carrier of P
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  (downarrow u) where u is Element of P : u in V  }  or X in bool the carrier of P )
assume  X in  {  (downarrow u) where u is Element of P : u in V  }  ; ::_thesis: X in bool the carrier of P
then  ex u being Element of P st
( X = downarrow u & u in V ) ;
hence  X in bool the carrier of P ; ::_thesis: verum
end;
reconsider u = u as Element of P by A1;
A3: downarrow u in  {  (downarrow u) where u is Element of P : u in V  }  by A1;
reconsider F =  {  (downarrow u) where u is Element of P : u in V  }  as Subset-Family of P by A2;
reconsider F = F as Subset-Family of P ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_downarrow_(inf_V)_implies_x_in_meet_F_)_&_(_x_in_meet_F_implies_x_in_downarrow_(inf_V)_)_)
let x be set ; ::_thesis: ( ( x in downarrow (inf V) implies x in meet F ) & ( x in meet F implies x in downarrow (inf V) ) )
hereby  ::_thesis: ( x in meet F implies x in downarrow (inf V) )
assume A4: x in downarrow (inf V) ; ::_thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d <= inf V by A4, WAYBEL_0:17;
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in F implies x in Y )
assume  Y in F ; ::_thesis: x in Y
then consider u being Element of P such that
A6: Y = downarrow u and
A7: u in V ;
 inf V is_<=_than V by YELLOW_0:33;
then  inf V <= u by A7, LATTICE3:def_8;
then  d <= u by A5, ORDERS_2:3;
hence  x in Y by A6, WAYBEL_0:17; ::_thesis: verum
end;
hence  x in meet F by A3, SETFAM_1:def_1; ::_thesis: verum
end;
assume A8: x in meet F ; ::_thesis: x in downarrow (inf V)
then reconsider d = x as Element of P ;
now__::_thesis:_for_b_being_Element_of_P_st_b_in_V_holds_
d_<=_b
let b be Element of P; ::_thesis: ( b in V implies d <= b )
assume  b in V ; ::_thesis: d <= b
then  downarrow b in F ;
then  d in downarrow b by A8, SETFAM_1:def_1;
hence  d <= b by WAYBEL_0:17; ::_thesis: verum
end;
then  d is_<=_than V by LATTICE3:def_8;
then  d <= inf V by YELLOW_0:33;
hence  x in downarrow (inf V) by WAYBEL_0:17; ::_thesis: verum
end;
hence  downarrow (inf V) = meet  {  (downarrow u) where u is Element of P : u in V  }  by TARSKI:1; ::_thesis: verum
end;

theorem :: WAYBEL14:16
for P being non empty complete Poset
for V being non empty Subset of P holds uparrow (sup V) = meet  {  (uparrow u) where u is Element of P : u in V  }
proof
let P be non empty complete Poset; ::_thesis: for V being non empty Subset of P holds uparrow (sup V) = meet  {  (uparrow u) where u is Element of P : u in V  }
let V be non empty Subset of P; ::_thesis: uparrow (sup V) = meet  {  (uparrow u) where u is Element of P : u in V  }
set F =  {  (uparrow u) where u is Element of P : u in V  }  ;
consider u being set  such that
A1: u in V by XBOOLE_0:def_1;
A2:  {  (uparrow u) where u is Element of P : u in V  }  c= bool the carrier of P
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  (uparrow u) where u is Element of P : u in V  }  or X in bool the carrier of P )
assume  X in  {  (uparrow u) where u is Element of P : u in V  }  ; ::_thesis: X in bool the carrier of P
then  ex u being Element of P st
( X = uparrow u & u in V ) ;
hence  X in bool the carrier of P ; ::_thesis: verum
end;
reconsider u = u as Element of P by A1;
A3: uparrow u in  {  (uparrow u) where u is Element of P : u in V  }  by A1;
reconsider F =  {  (uparrow u) where u is Element of P : u in V  }  as Subset-Family of P by A2;
reconsider F = F as Subset-Family of P ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_uparrow_(sup_V)_implies_x_in_meet_F_)_&_(_x_in_meet_F_implies_x_in_uparrow_(sup_V)_)_)
let x be set ; ::_thesis: ( ( x in uparrow (sup V) implies x in meet F ) & ( x in meet F implies x in uparrow (sup V) ) )
hereby  ::_thesis: ( x in meet F implies x in uparrow (sup V) )
assume A4: x in uparrow (sup V) ; ::_thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d >= sup V by A4, WAYBEL_0:18;
now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in F implies x in Y )
assume  Y in F ; ::_thesis: x in Y
then consider u being Element of P such that
A6: Y = uparrow u and
A7: u in V ;
 sup V is_>=_than V by YELLOW_0:32;
then  sup V >= u by A7, LATTICE3:def_9;
then  d >= u by A5, ORDERS_2:3;
hence  x in Y by A6, WAYBEL_0:18; ::_thesis: verum
end;
hence  x in meet F by A3, SETFAM_1:def_1; ::_thesis: verum
end;
assume A8: x in meet F ; ::_thesis: x in uparrow (sup V)
then reconsider d = x as Element of P ;
now__::_thesis:_for_b_being_Element_of_P_st_b_in_V_holds_
d_>=_b
let b be Element of P; ::_thesis: ( b in V implies d >= b )
assume  b in V ; ::_thesis: d >= b
then  uparrow b in F ;
then  d in uparrow b by A8, SETFAM_1:def_1;
hence  d >= b by WAYBEL_0:18; ::_thesis: verum
end;
then  d is_>=_than V by LATTICE3:def_9;
then  d >= sup V by YELLOW_0:32;
hence  x in uparrow (sup V) by WAYBEL_0:18; ::_thesis: verum
end;
hence  uparrow (sup V) = meet  {  (uparrow u) where u is Element of P : u in V  }  by TARSKI:1; ::_thesis: verum
end;

registration
let L be sup-Semilattice;
let x be Element of L;
cluster compactbelow x ->  directed ;
coherence
 compactbelow x is directed
proof
set cX = compactbelow x;
let xx, yy be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not xx in compactbelow x or not yy in compactbelow x or ex b1 being Element of the carrier of L st
( b1 in compactbelow x & xx <= b1 & yy <= b1 ) )
assume that
A1: xx in compactbelow x and
A2: yy in compactbelow x ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in compactbelow x & xx <= b1 & yy <= b1 )
set z = xx "\/" yy;
 yy is compact by A2, WAYBEL_8:4;
then  ( yy <= xx "\/" yy & yy << yy ) by WAYBEL_3:def_2, YELLOW_0:22;
then A3: yy << xx "\/" yy by WAYBEL_3:2;
 xx is compact by A1, WAYBEL_8:4;
then  ( xx <= xx "\/" yy & xx << xx ) by WAYBEL_3:def_2, YELLOW_0:22;
then  xx << xx "\/" yy by WAYBEL_3:2;
then  xx "\/" yy << xx "\/" yy by A3, WAYBEL_3:3;
then A4: xx "\/" yy is compact by WAYBEL_3:def_2;
take  xx "\/" yy ; ::_thesis: ( xx "\/" yy in compactbelow x & xx <= xx "\/" yy & yy <= xx "\/" yy )
 ( xx <= x & yy <= x ) by A1, A2, WAYBEL_8:4;
then  xx "\/" yy <= x by YELLOW_0:22;
hence  xx "\/" yy in compactbelow x by A4; ::_thesis: ( xx <= xx "\/" yy & yy <= xx "\/" yy )
thus  ( xx <= xx "\/" yy & yy <= xx "\/" yy ) by YELLOW_0:22; ::_thesis: verum
end;
end;

theorem Th17: :: WAYBEL14:17
for T being non empty TopSpace
for S being irreducible Subset of T
for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
proof
let T be non empty TopSpace; ::_thesis: for S being irreducible Subset of T
for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let S be irreducible Subset of T; ::_thesis: for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let V be Element of (InclPoset the topology of T); ::_thesis: ( V = S ` implies V is prime )
assume A1: V = S ` ; ::_thesis: V is prime
set sL = the topology of T;
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_6 ::_thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
A2: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then  ( X in the topology of T & Y in the topology of T ) ;
then reconsider X9 = X, Y9 = Y as Subset of T ;
 X9 /\ Y9 in the topology of T by A2, PRE_TOPC:def_1;
then A3: X /\ Y = X "/\" Y by YELLOW_1:9;
assume  X "/\" Y <= V ; ::_thesis: ( X <= V or Y <= V )
then  X /\ Y c= V by A3, YELLOW_1:3;
then  S c= (X9 /\ Y9) ` by A1, Lm1;
then  S c= (X9 `) \/ (Y9 `) by XBOOLE_1:54;
then  S = ((X9 `) \/ (Y9 `)) /\ S by XBOOLE_1:28;
then A4: S = ((X9 `) /\ S) \/ ((Y9 `) /\ S) by XBOOLE_1:23;
A5: S is closed by YELLOW_8:def_3;
 Y9 is open by A2, PRE_TOPC:def_2;
then  Y9 ` is closed ;
then A6: (Y9 `) /\ S is closed by A5;
 X9 is open by A2, PRE_TOPC:def_2;
then  X9 ` is closed ;
then  (X9 `) /\ S is closed by A5;
then  ( S = (X9 `) /\ S or S = (Y9 `) /\ S ) by A6, A4, YELLOW_8:def_3;
then  ( S c= X9 ` or S c= Y9 ` ) by XBOOLE_1:17;
then  ( X c= V or Y c= V ) by A1, Lm1;
hence  ( X <= V or Y <= V ) by YELLOW_1:3; ::_thesis: verum
end;

theorem Th18: :: WAYBEL14:18
for T being non empty TopSpace
for x, y being Element of (InclPoset the topology of T) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
proof
let T be non empty TopSpace; ::_thesis: for x, y being Element of (InclPoset the topology of T) holds
( x "\/" y = x \/ y & x "/\" y = x /\ y )
let x, y be Element of (InclPoset the topology of T); ::_thesis: ( x "\/" y = x \/ y & x "/\" y = x /\ y )
A1: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
then  ( x in the topology of T & y in the topology of T ) ;
then reconsider x9 = x, y9 = y as Subset of T ;
 ( x9 is open & y9 is open ) by A1, PRE_TOPC:def_2;
then  x9 \/ y9 is open ;
then  x9 \/ y9 in the topology of T by PRE_TOPC:def_2;
hence  x "\/" y = x \/ y by YELLOW_1:8; ::_thesis: x "/\" y = x /\ y
 x9 /\ y9 in the topology of T by A1, PRE_TOPC:def_1;
hence  x "/\" y = x /\ y by YELLOW_1:9; ::_thesis: verum
end;

theorem Th19: :: WAYBEL14:19
for T being non empty TopSpace
for V being Element of (InclPoset the topology of T) holds
( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
proof
let T be non empty TopSpace; ::_thesis: for V being Element of (InclPoset the topology of T) holds
( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
let V be Element of (InclPoset the topology of T); ::_thesis: ( V is prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) )
hereby  ::_thesis: ( ( for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) ) implies V is prime )
assume A1: V is prime ; ::_thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V )
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not X /\ Y c= V or X c= V or Y c= V )
assume A2: X /\ Y c= V ; ::_thesis: ( X c= V or Y c= V )
 X /\ Y = X "/\" Y by Th18;
then  X "/\" Y <= V by A2, YELLOW_1:3;
then  ( X <= V or Y <= V ) by A1, WAYBEL_6:def_6;
hence  ( X c= V or Y c= V ) by YELLOW_1:3; ::_thesis: verum
end;
assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not X /\ Y c= V or X c= V or Y c= V ) ; ::_thesis: V is prime
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def_6 ::_thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
assume A4: X "/\" Y <= V ; ::_thesis: ( X <= V or Y <= V )
 X /\ Y = X "/\" Y by Th18;
then  X /\ Y c= V by A4, YELLOW_1:3;
then  ( X c= V or Y c= V ) by A3;
hence  ( X <= V or Y <= V ) by YELLOW_1:3; ::_thesis: verum
end;

theorem :: WAYBEL14:20
for T being non empty TopSpace
for V being Element of (InclPoset the topology of T) holds
( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
proof
let T be non empty TopSpace; ::_thesis: for V being Element of (InclPoset the topology of T) holds
( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
let V be Element of (InclPoset the topology of T); ::_thesis: ( V is co-prime iff for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) )
hereby  ::_thesis: ( ( for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ) implies V is co-prime )
assume A1: V is co-prime ; ::_thesis: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y )
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not V c= X \/ Y or V c= X or V c= Y )
assume A2: V c= X \/ Y ; ::_thesis: ( V c= X or V c= Y )
 X \/ Y = X "\/" Y by Th18;
then  V <= X "\/" Y by A2, YELLOW_1:3;
then  ( V <= X or V <= Y ) by A1, Th14;
hence  ( V c= X or V c= Y ) by YELLOW_1:3; ::_thesis: verum
end;
assume A3: for X, Y being Element of (InclPoset the topology of T) holds
( not V c= X \/ Y or V c= X or V c= Y ) ; ::_thesis: V is co-prime
now__::_thesis:_for_X,_Y_being_Element_of_(InclPoset_the_topology_of_T)_holds_
(_not_V_<=_X_"\/"_Y_or_V_<=_X_or_V_<=_Y_)
let X, Y be Element of (InclPoset the topology of T); ::_thesis: ( not V <= X "\/" Y or V <= X or V <= Y )
assume A4: V <= X "\/" Y ; ::_thesis: ( V <= X or V <= Y )
 X \/ Y = X "\/" Y by Th18;
then  V c= X \/ Y by A4, YELLOW_1:3;
then  ( V c= X or V c= Y ) by A3;
hence  ( V <= X or V <= Y ) by YELLOW_1:3; ::_thesis: verum
end;
hence  V is co-prime by Th14; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster InclPoset the topology of T ->  distributive ;
coherence
 InclPoset the topology of T is distributive
proof
let x, y, z be Element of (InclPoset the topology of T); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th18
.= x /\ (y \/ z) by Th18
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by Th18
.= (x "/\" y) \/ (x "/\" z) by Th18
.= (x "/\" y) "\/" (x "/\" z) by Th18 ; ::_thesis: verum
end;
end;

theorem Th21: :: WAYBEL14:21
for T being non empty TopSpace
for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
proof
let T be non empty TopSpace; ::_thesis: for L being TopLattice
for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let L be TopLattice; ::_thesis: for t being Point of T
for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let t be Point of T; ::_thesis: for l being Point of L
for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let l be Point of L; ::_thesis: for X being Subset-Family of L st TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l holds
X is Basis of t
let X be Subset-Family of L; ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) & t = l & X is Basis of l implies X is Basis of t )
assume A1: TopStruct(# the carrier of T, the topology of T #) = TopStruct(# the carrier of L, the topology of L #) ; ::_thesis: ( not t = l or not X is Basis of l or X is Basis of t )
then reconsider X9 = X as Subset-Family of T ;
assume A2: t = l ; ::_thesis: ( not X is Basis of l or X is Basis of t )
assume A3: X is Basis of l ; ::_thesis: X is Basis of t
then A4: X c= the topology of L by TOPS_2:64;
A5: l in Intersect X by A3, YELLOW_8:def_1;
A6: for S being Subset of L st S is open & l in S holds
ex V being Subset of L st
( V in X & V c= S ) by A3, YELLOW_8:def_1;
now__::_thesis:_for_S_being_Subset_of_T_st_S_is_open_&_t_in_S_holds_
ex_V_being_Subset_of_T_st_
(_V_in_X9_&_V_c=_S_)
let S be Subset of T; ::_thesis: ( S is open & t in S implies ex V being Subset of T st
( V in X9 & V c= S ) )
assume that
A7: S is open and
A8: t in S ; ::_thesis: ex V being Subset of T st
( V in X9 & V c= S )
reconsider S9 = S as Subset of L by A1;
 S in the topology of T by A7, PRE_TOPC:def_2;
then  S9 is open by A1, PRE_TOPC:def_2;
then consider V being Subset of L such that
A9: ( V in X & V c= S9 ) by A2, A6, A8;
reconsider V = V as Subset of T by A1;
take V = V; ::_thesis: ( V in X9 & V c= S )
thus  ( V in X9 & V c= S ) by A9; ::_thesis: verum
end;
hence  X is Basis of t by A1, A2, A4, A5, TOPS_2:64, YELLOW_8:def_1; ::_thesis: verum
end;

theorem Th22: :: WAYBEL14:22
for L being TopLattice
for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact
proof
let L be TopLattice; ::_thesis: for x being Element of L st ( for X being Subset of L st X is open holds
X is upper ) holds
uparrow x is compact
let x be Element of L; ::_thesis: ( ( for X being Subset of L st X is open holds
X is upper ) implies uparrow x is compact )
assume A1: for X being Subset of L st X is open holds
X is upper ; ::_thesis: uparrow x is compact
set P = uparrow x;
let F be Subset-Family of L; :: according to COMPTS_1:def_4 ::_thesis: ( not F is Cover of uparrow x or not F is open or ex b1 being Element of bool (bool the carrier of L) st
( b1 c= F & b1 is Cover of uparrow x & b1 is finite ) )
assume that
A2: F is Cover of uparrow x and
A3: F is open ; ::_thesis: ex b1 being Element of bool (bool the carrier of L) st
( b1 c= F & b1 is Cover of uparrow x & b1 is finite )
 x <= x ;
then A4: x in uparrow x by WAYBEL_0:18;
 uparrow x c= union F by A2, SETFAM_1:def_11;
then consider Y being set  such that
A5: x in Y and
A6: Y in F by A4, TARSKI:def_4;
reconsider Y = Y as Subset of L by A6;
reconsider G = {Y} as Subset-Family of L ;
reconsider G = G as Subset-Family of L ;
take  G ; ::_thesis: ( G c= F & G is Cover of uparrow x & G is finite )
thus  G c= F by A6, ZFMISC_1:31; ::_thesis: ( G is Cover of uparrow x & G is finite )
 Y is open by A3, A6, TOPS_2:def_1;
then  Y is upper by A1;
then  uparrow x c= Y by A5, WAYBEL11:42;
hence  uparrow x c= union G by ZFMISC_1:25; :: according to SETFAM_1:def_11 ::_thesis: G is finite
thus  G is finite ; ::_thesis: verum
end;

begin


registration
let L be complete LATTICE;
cluster sigma L ->  non empty ;
coherence
 not sigma L is empty
proof
 sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
hence  not sigma L is empty ; ::_thesis: verum
end;
end;

theorem Th23: :: WAYBEL14:23
for L being complete Scott TopLattice holds sigma L = the topology of L
proof
let L be complete Scott TopLattice; ::_thesis: sigma L = the topology of L
 TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
hence  sigma L = the topology of L by WAYBEL11:def_12; ::_thesis: verum
end;

theorem Th24: :: WAYBEL14:24
for L being complete Scott TopLattice
for X being Subset of L holds
( X in sigma L iff X is open )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L holds
( X in sigma L iff X is open )
let X be Subset of L; ::_thesis: ( X in sigma L iff X is open )
 sigma L = the topology of L by Th23;
hence  ( X in sigma L iff X is open ) by PRE_TOPC:def_2; ::_thesis: verum
end;

Lm2:  for L being complete Scott TopLattice
for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F =  {  (downarrow u) where u is Element of L : u in V  }  & CF = COMPLEMENT F holds
CF is directed
proof
let L be complete Scott TopLattice; ::_thesis: for V being filtered Subset of L
for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F =  {  (downarrow u) where u is Element of L : u in V  }  & CF = COMPLEMENT F holds
CF is directed
let V be filtered Subset of L; ::_thesis: for F being Subset-Family of L
for CF being Subset of (InclPoset (sigma L)) st F =  {  (downarrow u) where u is Element of L : u in V  }  & CF = COMPLEMENT F holds
CF is directed
let F be Subset-Family of L; ::_thesis: for CF being Subset of (InclPoset (sigma L)) st F =  {  (downarrow u) where u is Element of L : u in V  }  & CF = COMPLEMENT F holds
CF is directed
let CF be Subset of (InclPoset (sigma L)); ::_thesis: ( F =  {  (downarrow u) where u is Element of L : u in V  }  & CF = COMPLEMENT F implies CF is directed )
assume that
A1: F =  {  (downarrow u) where u is Element of L : u in V  }  and
A2: CF = COMPLEMENT F ; ::_thesis: CF is directed
set IPs = InclPoset (sigma L);
let x, y be Element of (InclPoset (sigma L)); :: according to WAYBEL_0:def_1 ::_thesis: ( not x in CF or not y in CF or ex b1 being Element of the carrier of (InclPoset (sigma L)) st
( b1 in CF & x <= b1 & y <= b1 ) )
assume that
A3: x in CF and
A4: y in CF ; ::_thesis: ex b1 being Element of the carrier of (InclPoset (sigma L)) st
( b1 in CF & x <= b1 & y <= b1 )
A5: sigma L = the topology of L by Th23;
then A6: the carrier of (InclPoset (sigma L)) = the topology of L by YELLOW_1:1;
then  ( x in sigma L & y in sigma L ) by A5;
then reconsider x9 = x, y9 = y as Subset of L ;
 x9 ` in F by A2, A3, SETFAM_1:def_7;
then consider ux being Element of L such that
A7: x9 ` = downarrow ux and
A8: ux in V by A1;
 y9 ` in F by A2, A4, SETFAM_1:def_7;
then consider uy being Element of L such that
A9: y9 ` = downarrow uy and
A10: uy in V by A1;
consider uz being Element of L such that
A11: uz in V and
A12: uz <= ux and
A13: uz <= uy by A8, A10, WAYBEL_0:def_2;
 (downarrow uz) ` is open by WAYBEL11:12;
then reconsider z = (downarrow uz) ` as Element of (InclPoset (sigma L)) by A6, PRE_TOPC:def_2;
take  z ; ::_thesis: ( z in CF & x <= z & y <= z )
 downarrow uz in F by A1, A11;
hence  z in CF by A2, YELLOW_8:5; ::_thesis: ( x <= z & y <= z )
 downarrow uz c= downarrow uy by A13, WAYBEL_0:21;
then A14: (downarrow uy) ` c= (downarrow uz) ` by SUBSET_1:12;
 downarrow uz c= downarrow ux by A12, WAYBEL_0:21;
then  (downarrow ux) ` c= (downarrow uz) ` by SUBSET_1:12;
hence  ( x <= z & y <= z ) by A7, A9, A14, YELLOW_1:3; ::_thesis: verum
end;

theorem Th25: :: WAYBEL14:25
for L being complete Scott TopLattice
for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV =  {  ((downarrow x) `) where x is Element of L : x in X  }  holds
VV is directed
proof
let L be complete Scott TopLattice; ::_thesis: for VV being Subset of (InclPoset (sigma L))
for X being filtered Subset of L st VV =  {  ((downarrow x) `) where x is Element of L : x in X  }  holds
VV is directed
let VV be Subset of (InclPoset (sigma L)); ::_thesis: for X being filtered Subset of L st VV =  {  ((downarrow x) `) where x is Element of L : x in X  }  holds
VV is directed
let V be filtered Subset of L; ::_thesis: ( VV =  {  ((downarrow x) `) where x is Element of L : x in V  }  implies VV is directed )
set F =  {  (downarrow u) where u is Element of L : u in V  }  ;
  {  (downarrow u) where u is Element of L : u in V  }  c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (downarrow u) where u is Element of L : u in V  }  or x in bool the carrier of L )
assume  x in  {  (downarrow u) where u is Element of L : u in V  }  ; ::_thesis: x in bool the carrier of L
then  ex u being Element of L st
( x = downarrow u & u in V ) ;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider F =  {  (downarrow u) where u is Element of L : u in V  }  as Subset-Family of L ;
reconsider F = F as Subset-Family of L ;
assume A1: VV =  {  ((downarrow x) `) where x is Element of L : x in V  }  ; ::_thesis: VV is directed
 VV c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in VV or x in bool the carrier of L )
assume  x in VV ; ::_thesis: x in bool the carrier of L
then  ex u being Element of L st
( x = (downarrow u) ` & u in V ) by A1;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider VV = VV as Subset-Family of L ;
reconsider VV = VV as Subset-Family of L ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_VV_implies_x_in_COMPLEMENT_F_)_&_(_x_in_COMPLEMENT_F_implies_x_in_VV_)_)
let x be set ; ::_thesis: ( ( x in VV implies x in COMPLEMENT F ) & ( x in COMPLEMENT F implies x in VV ) )
hereby  ::_thesis: ( x in COMPLEMENT F implies x in VV )
assume  x in VV ; ::_thesis: x in COMPLEMENT F
then consider u being Element of L such that
A2: x = (downarrow u) ` and
A3: u in V by A1;
 downarrow u in F by A3;
hence  x in COMPLEMENT F by A2, YELLOW_8:5; ::_thesis: verum
end;
assume A4: x in COMPLEMENT F ; ::_thesis: x in VV
then reconsider X = x as Subset of L ;
 X ` in F by A4, SETFAM_1:def_7;
then consider u being Element of L such that
A5: X ` = downarrow u and
A6: u in V ;
 X = (downarrow u) ` by A5;
hence  x in VV by A1, A6; ::_thesis: verum
end;
then  VV = COMPLEMENT F by TARSKI:1;
hence  VV is directed by Lm2; ::_thesis: verum
end;

theorem Th26: :: WAYBEL14:26
for L being complete Scott TopLattice
for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x
let x be Element of L; ::_thesis: for X being Subset of L st X is open & x in X holds
inf X << x
let X be Subset of L; ::_thesis: ( X is open & x in X implies inf X << x )
assume that
A1: X is open and
A2: x in X ; ::_thesis: inf X << x
A3: ( X is upper & X is property(S) ) by A1, WAYBEL11:15;
now__::_thesis:_for_D_being_non_empty_directed_Subset_of_L_st_x_<=_sup_D_holds_
ex_y_being_Element_of_L_st_
(_y_in_D_&_inf_X_<=_y_)
let D be non empty directed Subset of L; ::_thesis: ( x <= sup D implies ex y being Element of L st
( y in D & inf X <= y ) )
assume  x <= sup D ; ::_thesis: ex y being Element of L st
( y in D & inf X <= y )
then  sup D in X by A2, A3, WAYBEL_0:def_20;
then consider y being Element of L such that
A4: y in D and
A5: for x being Element of L st x in D & x >= y holds
x in X by A3, WAYBEL11:def_3;
take y = y; ::_thesis: ( y in D & inf X <= y )
thus  y in D by A4; ::_thesis: inf X <= y
 y <= y ;
then  ( inf X is_<=_than X & y in X ) by A4, A5, YELLOW_0:33;
hence  inf X <= y by LATTICE3:def_8; ::_thesis: verum
end;
hence  inf X << x by WAYBEL_3:def_1; ::_thesis: verum
end;

definition
let R be non empty reflexive RelStr ;
let f be Function of [:R,R:],R;
attrf is jointly_Scott-continuous  means :Def1: :: WAYBEL14:def 1
 for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds
ex ft being Function of [:T,T:],T st
( ft = f & ft is continuous );
end;

:: deftheorem Def1 defines jointly_Scott-continuous WAYBEL14:def_1_:_
 for R being non empty reflexive RelStr
for f being Function of [:R,R:],R holds
( f is jointly_Scott-continuous iff for T being non empty TopSpace st TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence R) holds
ex ft being Function of [:T,T:],T st
( ft = f & ft is continuous ) );

theorem Th27: :: WAYBEL14:27
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X holds
( V is co-prime iff ( X is filtered & X is upper ) )
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X implies ( V is co-prime iff ( X is filtered & X is upper ) ) )
assume A1: V = X ; ::_thesis: ( V is co-prime iff ( X is filtered & X is upper ) )
A2: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
A3: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
A4: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A5: X is upper by A1, A3, WAYBEL11:31;
hereby  ::_thesis: ( X is filtered & X is upper implies V is co-prime )
assume A6: V is co-prime ; ::_thesis: ( X is filtered & X is upper )
thus  X is filtered ::_thesis: X is upper
proof
let v, w be Element of L; :: according to WAYBEL_0:def_2 ::_thesis: ( not v in X or not w in X or ex b1 being Element of the carrier of L st
( b1 in X & b1 <= v & b1 <= w ) )
assume that
A7: v in X and
A8: w in X ; ::_thesis: ex b1 being Element of the carrier of L st
( b1 in X & b1 <= v & b1 <= w )
 ( (downarrow w) ` is open & (downarrow v) ` is open ) by WAYBEL11:12;
then reconsider mdw = (downarrow w) ` , mdv = (downarrow v) ` as Element of (InclPoset (sigma L)) by A3, A4, A2, PRE_TOPC:def_2;
 w <= w ;
then  w in downarrow w by WAYBEL_0:17;
then  not V c= (downarrow w) ` by A1, A8, XBOOLE_0:def_5;
then A9: not V <= mdw by YELLOW_1:3;
 v <= v ;
then  v in downarrow v by WAYBEL_0:17;
then  not V c= (downarrow v) ` by A1, A7, XBOOLE_0:def_5;
then  not V <= mdv by YELLOW_1:3;
then  not V <= mdv "\/" mdw by A3, A6, A9, Th14;
then A10: not V c= mdv "\/" mdw by YELLOW_1:3;
take z = v "/\" w; ::_thesis: ( z in X & z <= v & z <= w )
A11: mdv \/ mdw = ((downarrow v) /\ (downarrow w)) ` by XBOOLE_1:54
.= (downarrow (v "/\" w)) ` by Th3 ;
 mdv \/ mdw c= mdv "\/" mdw by A3, YELLOW_1:6;
then  not V c= mdv \/ mdw by A10, XBOOLE_1:1;
then  X meets ((downarrow (v "/\" w)) `) ` by A1, A11, SUBSET_1:24;
then  X /\ (((downarrow (v "/\" w)) `) `) <> {} by XBOOLE_0:def_7;
then consider zz being set  such that
A12: zz in X /\ (downarrow (v "/\" w)) by XBOOLE_0:def_1;
A13: zz in downarrow (v "/\" w) by A12, XBOOLE_0:def_4;
A14: zz in X by A12, XBOOLE_0:def_4;
reconsider zz = zz as Element of L by A12;
 zz <= v "/\" w by A13, WAYBEL_0:17;
hence  z in X by A5, A14, WAYBEL_0:def_20; ::_thesis: ( z <= v & z <= w )
thus  ( z <= v & z <= w ) by YELLOW_0:23; ::_thesis: verum
end;
thus  X is upper by A1, A3, A4, WAYBEL11:31; ::_thesis: verum
end;
assume A15: ( X is filtered & X is upper ) ; ::_thesis: V is co-prime
assume  not V is co-prime ; ::_thesis: contradiction
then consider Xx, Y being Element of (InclPoset (sigma L)) such that
A16: V <= Xx "\/" Y and
A17: not V <= Xx and
A18: not V <= Y by A3, Th14;
 ( Xx in sigma L & Y in sigma L ) by A4;
then reconsider Xx9 = Xx, Y9 = Y as Subset of L ;
A19: Y9 is open by A3, A4, A2, PRE_TOPC:def_2;
then A20: Y9 is upper by WAYBEL11:def_4;
A21: Xx9 is open by A3, A4, A2, PRE_TOPC:def_2;
then  Xx9 \/ Y9 is open by A19;
then  Xx \/ Y in sigma L by A3, A2, PRE_TOPC:def_2;
then  Xx \/ Y = Xx "\/" Y by YELLOW_1:8;
then A22: V c= Xx \/ Y by A16, YELLOW_1:3;
 not V c= Y by A18, YELLOW_1:3;
then consider w being set  such that
A23: w in V and
A24: not w in Y by TARSKI:def_3;
 not V c= Xx by A17, YELLOW_1:3;
then consider v being set  such that
A25: v in V and
A26: not v in Xx by TARSKI:def_3;
reconsider v = v, w = w as Element of L by A1, A25, A23;
A27: Xx9 is upper by A21, WAYBEL11:def_4;
A28: now__::_thesis:_not_v_"/\"_w_in_Xx9_\/_Y9
assume A29: v "/\" w in Xx9 \/ Y9 ; ::_thesis: contradiction
percases ( v "/\" w in Xx9 or v "/\" w in Y9 ) by A29, XBOOLE_0:def_3;
supposeA30: v "/\" w in Xx9 ; ::_thesis: contradiction
 v "/\" w <= v by YELLOW_0:23;
hence  contradiction by A26, A27, A30, WAYBEL_0:def_20; ::_thesis: verum
end;
supposeA31: v "/\" w in Y9 ; ::_thesis: contradiction
 v "/\" w <= w by YELLOW_0:23;
hence  contradiction by A24, A20, A31, WAYBEL_0:def_20; ::_thesis: verum
end;
end;
end;
 v "/\" w in X by A1, A15, A25, A23, WAYBEL_0:41;
hence  contradiction by A1, A22, A28; ::_thesis: verum
end;

theorem :: WAYBEL14:28
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X & ex x being Element of L st X = (downarrow x) ` holds
( V is prime & V <> the carrier of L )
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X & ex x being Element of L st X = (downarrow x) ` implies ( V is prime & V <> the carrier of L ) )
assume A1: V = X ; ::_thesis: ( for x being Element of L holds not X = (downarrow x) ` or ( V is prime & V <> the carrier of L ) )
A2: ( sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) & TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) ) by WAYBEL11:32, WAYBEL11:def_12;
given u being Element of L such that A3: X = (downarrow u) ` ; ::_thesis: ( V is prime & V <> the carrier of L )
 ( Cl {u} = downarrow u & Cl {u} is irreducible ) by WAYBEL11:9, YELLOW_8:17;
hence  V is prime by A1, A2, A3, Th17; ::_thesis: V <> the carrier of L
assume  V = the carrier of L ; ::_thesis: contradiction
hence  contradiction by A1, A3, Th2; ::_thesis: verum
end;

theorem Th29: :: WAYBEL14:29
for L being complete Scott TopLattice
for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L
for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let X be Subset of L; ::_thesis: for V being Element of (InclPoset (sigma L)) st V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L holds
ex x being Element of L st X = (downarrow x) `
let V be Element of (InclPoset (sigma L)); ::_thesis: ( V = X & sup_op L is jointly_Scott-continuous & V is prime & V <> the carrier of L implies ex x being Element of L st X = (downarrow x) ` )
assume that
A1: V = X and
A2: sup_op L is jointly_Scott-continuous and
A3: V is prime and
A4: V <> the carrier of L ; ::_thesis: ex x being Element of L st X = (downarrow x) `
A5: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
set A = X ` ;
A6: sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) by WAYBEL11:def_12;
A7: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
then A8: X is open by A1, A6, A5, PRE_TOPC:def_2;
then  X ` is closed ;
then A9: ( X ` is directly_closed & X ` is lower ) by WAYBEL11:7;
A10: X ` is directed
proof
set LxL = [:L,L:];
given a, b being Element of L such that A11: ( a in X ` & b in X ` ) and
A12: for z being Element of L holds
( not z in X ` or not a <= z or not b <= z ) ; :: according to WAYBEL_0:def_1 ::_thesis: contradiction
 ( a <= a "\/" b & b <= a "\/" b ) by YELLOW_0:22;
then  not a "\/" b in X ` by A12;
then A13: a "\/" b in X by XBOOLE_0:def_5;
consider Tsup being Function of [:L,L:],L such that
A14: Tsup = sup_op L and
A15: Tsup is continuous by A2, A5, Def1;
A16: Tsup . (a,b) = a "\/" b by A14, WAYBEL_2:def_5;
 [#] L <> {} ;
then  Tsup " X is open by A8, A15, TOPS_2:43;
then consider AA being Subset-Family of [:L,L:] such that
A17: Tsup " X = union AA and
A18: for e being set st e in AA holds
ex X1, Y1 being Subset of L st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A19: the carrier of [:L,L:] = [: the carrier of L, the carrier of L:] by BORSUK_1:def_2;
then  [a,b] in the carrier of [:L,L:] by ZFMISC_1:def_2;
then  [a,b] in Tsup " X by A13, A16, FUNCT_2:38;
then consider AAe being set  such that
A20: [a,b] in AAe and
A21: AAe in AA by A17, TARSKI:def_4;
consider Va, Vb being Subset of L such that
A22: AAe = [:Va,Vb:] and
A23: Va is open and
A24: Vb is open by A18, A21;
A25: ( a in Va & b in Vb ) by A20, A22, ZFMISC_1:87;
reconsider Va9 = Va, Vb9 = Vb as Subset of L ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_Tsup_.:_AAe_implies_x_in_Va_/\_Vb_)_&_(_x_in_Va_/\_Vb_implies_x_in_Tsup_.:_AAe_)_)
let x be set ; ::_thesis: ( ( x in Tsup .: AAe implies x in Va /\ Vb ) & ( x in Va /\ Vb implies x in Tsup .: AAe ) )
hereby  ::_thesis: ( x in Va /\ Vb implies x in Tsup .: AAe )
assume  x in Tsup .: AAe ; ::_thesis: x in Va /\ Vb
then consider cd being set  such that
A26: cd in the carrier of [:L,L:] and
A27: cd in AAe and
A28: Tsup . cd = x by FUNCT_2:64;
consider c, d being Element of L such that
A29: cd = [c,d] by A19, A26, DOMAIN_1:1;
reconsider c = c, d = d as Element of L ;
A30: x = Tsup . (c,d) by A28, A29
.= c "\/" d by A14, WAYBEL_2:def_5 ;
A31: ( d <= c "\/" d & Vb9 is upper ) by A24, WAYBEL11:def_4, YELLOW_0:22;
 d in Vb by A22, A27, A29, ZFMISC_1:87;
then A32: x in Vb by A30, A31, WAYBEL_0:def_20;
A33: ( c <= c "\/" d & Va9 is upper ) by A23, WAYBEL11:def_4, YELLOW_0:22;
 c in Va by A22, A27, A29, ZFMISC_1:87;
then  x in Va by A30, A33, WAYBEL_0:def_20;
hence  x in Va /\ Vb by A32, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A34: x in Va /\ Vb ; ::_thesis: x in Tsup .: AAe
then reconsider c = x as Element of L ;
 ( x in Va & x in Vb ) by A34, XBOOLE_0:def_4;
then A35: [c,c] in AAe by A22, ZFMISC_1:87;
 c <= c ;
then  c = c "\/" c by YELLOW_0:24;
then A36: c = Tsup . (c,c) by A14, WAYBEL_2:def_5;
 [c,c] in the carrier of [:L,L:] by A19, ZFMISC_1:87;
hence  x in Tsup .: AAe by A35, A36, FUNCT_2:35; ::_thesis: verum
end;
then A37: Tsup .: AAe = Va /\ Vb by TARSKI:1;
A38: Tsup .: (Tsup " X) c= X by FUNCT_1:75;
 Tsup .: AAe c= Tsup .: (Tsup " X) by A17, A21, RELAT_1:123, ZFMISC_1:74;
then A39: Tsup .: AAe c= X by A38, XBOOLE_1:1;
 ( Va in sigma L & Vb in sigma L ) by A6, A5, A23, A24, PRE_TOPC:def_2;
then  ( Va c= X or Vb c= X ) by A1, A3, A6, A7, A37, A39, Th19;
hence  contradiction by A11, A25, XBOOLE_0:def_5; ::_thesis: verum
end;
take u = sup (X `); ::_thesis: X = (downarrow u) `
now__::_thesis:_not_X_`_=_{}
assume  X ` = {} ; ::_thesis: contradiction
then  (X `) ` = the carrier of L ;
hence  contradiction by A1, A4; ::_thesis: verum
end;
then  u in X ` by A9, A10, WAYBEL11:def_2;
then  X ` = downarrow u by A9, Th5;
hence  X = (downarrow u) ` ; ::_thesis: verum
end;

theorem Th30: :: WAYBEL14:30
for L being complete Scott TopLattice st L is continuous holds
sup_op L is jointly_Scott-continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies sup_op L is jointly_Scott-continuous )
assume A1: L is continuous ; ::_thesis: sup_op L is jointly_Scott-continuous
set Tsup = sup_op L;
let T be non empty TopSpace; :: according to WAYBEL14:def_1 ::_thesis: ( TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence L) implies ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous ) )
assume A2: TopStruct(# the carrier of T, the topology of T #) = ConvergenceSpace (Scott-Convergence L) ; ::_thesis: ex ft being Function of [:T,T:],T st
( ft = sup_op L & ft is continuous )
A3: the carrier of [:T,T:] = [: the carrier of T, the carrier of T:] by BORSUK_1:def_2;
A4: the carrier of T = the carrier of L by A2, YELLOW_6:def_24;
then  the carrier of [:T,T:] = the carrier of [:L,L:] by A3, YELLOW_3:def_2;
then reconsider Tsup = sup_op L as Function of [:T,T:],T by A4;
take  Tsup ; ::_thesis: ( Tsup = sup_op L & Tsup is continuous )
thus  Tsup = sup_op L ; ::_thesis: Tsup is continuous
A5: TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) by WAYBEL11:32;
 for x being Point of [:T,T:] holds Tsup is_continuous_at x
proof
reconsider Lc = L as complete continuous Scott TopLattice by A1;
let ab be Point of [:T,T:]; ::_thesis: Tsup is_continuous_at ab
reconsider Tsab = Tsup . ab as Point of T ;
consider a, b being Point of T such that
A6: ab = [a,b] by A3, DOMAIN_1:1;
reconsider a9 = a, b9 = b as Element of L by A2, YELLOW_6:def_24;
set D1 = waybelow a9;
set D2 = waybelow b9;
set D = (waybelow a9) "\/" (waybelow b9);
reconsider Tsab9 = Tsab as Element of L by A2, YELLOW_6:def_24;
let G be a_neighborhood of Tsup . ab; :: according to TMAP_1:def_2 ::_thesis: ex b1 being a_neighborhood of ab st Tsup .: b1 c= G
A7: Tsab in Int G by CONNSP_2:def_1;
reconsider basab =  {  (wayabove q) where q is Element of L : q << Tsab9  }  as Basis of Tsab9 by A1, WAYBEL11:44;
 basab is Basis of Tsab by A2, A5, Th21;
then consider V being Subset of T such that
A8: V in basab and
A9: V c= Int G by A7, YELLOW_8:def_1;
consider u being Element of L such that
A10: V = wayabove u and
A11: u << Tsab9 by A8;
A12: (waybelow a9) "\/" (waybelow b9) =  {  (x "\/" y) where x, y is Element of L : ( x in waybelow a9 & y in waybelow b9 )  }  by YELLOW_4:def_3;
 Lc = L ;
then A13: ( a9 = sup (waybelow a9) & b9 = sup (waybelow b9) ) by WAYBEL_3:def_5;
Tsab9 = Tsup . (a,b) by A6
.= a9 "\/" b9 by WAYBEL_2:def_5
.= sup ((waybelow a9) "\/" (waybelow b9)) by A13, WAYBEL_2:4 ;
then consider xy being Element of L such that
A14: xy in (waybelow a9) "\/" (waybelow b9) and
A15: u << xy by A1, A11, WAYBEL_4:53;
consider x, y being Element of L such that
A16: xy = x "\/" y and
A17: x in waybelow a9 and
A18: y in waybelow b9 by A14, A12;
reconsider H = [:(wayabove x),(wayabove y):] as Subset of [:T,T:] by A4, A3, YELLOW_3:def_2;
 y << b9 by A18, WAYBEL_3:7;
then A19: b9 in wayabove y ;
 Int G c= G by TOPS_1:16;
then A20: V c= G by A9, XBOOLE_1:1;
reconsider wx = wayabove x, wy = wayabove y as Subset of T by A2, YELLOW_6:def_24;
 wayabove y is open by A1, WAYBEL11:36;
then  wayabove y in the topology of L by PRE_TOPC:def_2;
then A21: wy is open by A2, A5, PRE_TOPC:def_2;
 wayabove x is open by A1, WAYBEL11:36;
then  wayabove x in the topology of L by PRE_TOPC:def_2;
then  wx is open by A2, A5, PRE_TOPC:def_2;
then  H is open by A21, BORSUK_1:6;
then A22: H = Int H by TOPS_1:23;
 x << a9 by A17, WAYBEL_3:7;
then  a9 in wayabove x ;
then  [a9,b9] in H by A19, ZFMISC_1:87;
then reconsider H = H as a_neighborhood of ab by A6, A22, CONNSP_2:def_1;
take  H ; ::_thesis: Tsup .: H c= G
A23: ( Tsup .: H = (wayabove x) "\/" (wayabove y) & (wayabove x) "\/" (wayabove y) c= uparrow (x "\/" y) ) by Th12, WAYBEL_2:35;
 uparrow (x "\/" y) c= wayabove u by A15, A16, Th7;
then  Tsup .: H c= V by A10, A23, XBOOLE_1:1;
hence  Tsup .: H c= G by A20, XBOOLE_1:1; ::_thesis: verum
end;
hence  Tsup is continuous by TMAP_1:44; ::_thesis: verum
end;

theorem Th31: :: WAYBEL14:31
for L being complete Scott TopLattice st sup_op L is jointly_Scott-continuous holds
L is sober
proof
let L be complete Scott TopLattice; ::_thesis: ( sup_op L is jointly_Scott-continuous implies L is sober )
assume A1: sup_op L is jointly_Scott-continuous ; ::_thesis: L is sober
let S be irreducible Subset of L; :: according to YELLOW_8:def_5 ::_thesis: ex b1 being Element of the carrier of L st
( b1 is_dense_point_of S & ( for b2 being Element of the carrier of L holds
( not b2 is_dense_point_of S or b1 = b2 ) ) )
A2: ( sigma L = the topology of (ConvergenceSpace (Scott-Convergence L)) & TopStruct(# the carrier of L, the topology of L #) = ConvergenceSpace (Scott-Convergence L) ) by WAYBEL11:32, WAYBEL11:def_12;
A3: ( not S is empty & S is closed ) by YELLOW_8:def_3;
then  ( the carrier of (InclPoset (sigma L)) = sigma L & S ` is open ) by YELLOW_1:1;
then reconsider V = S ` as Element of (InclPoset (sigma L)) by A2, PRE_TOPC:def_2;
 S ` <> the carrier of L by Th2;
then consider p being Element of L such that
A4: V = (downarrow p) ` by A1, A2, Th17, Th29;
A5: L is T_0 by WAYBEL11:10;
take  p ; ::_thesis: ( p is_dense_point_of S & ( for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 ) ) )
A6: Cl {p} = downarrow p by WAYBEL11:9;
A7: S = downarrow p by A4, TOPS_1:1;
hence  p is_dense_point_of S by A6, YELLOW_8:18; ::_thesis: for b1 being Element of the carrier of L holds
( not b1 is_dense_point_of S or p = b1 )
let q be Point of L; ::_thesis: ( not q is_dense_point_of S or p = q )
assume  q is_dense_point_of S ; ::_thesis: p = q
then  Cl {q} = S by A3, YELLOW_8:16;
hence  p = q by A7, A6, A5, YELLOW_8:23; ::_thesis: verum
end;

theorem :: WAYBEL14:32
for L being complete Scott TopLattice st L is continuous holds
( L is compact & L is locally-compact & L is sober & L is Baire )
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies ( L is compact & L is locally-compact & L is sober & L is Baire ) )
assume A1: L is continuous ; ::_thesis: ( L is compact & L is locally-compact & L is sober & L is Baire )
A2: ( uparrow (Bottom L) = the carrier of L & [#] L = the carrier of L ) by Th10;
A3: for X being Subset of L st X is open holds
X is upper by WAYBEL11:def_4;
then  uparrow (Bottom L) is compact by Th22;
hence  L is compact by A2, COMPTS_1:1; ::_thesis: ( L is locally-compact & L is sober & L is Baire )
thus A4: L is locally-compact ::_thesis: ( L is sober & L is Baire )
proof
let x be Point of L; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of bool the carrier of L holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of L st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of L; ::_thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume that
A5: x in X and
A6: X is open ; ::_thesis: ex b1 being Element of bool the carrier of L st
( x in Int b1 & b1 c= X & b1 is compact )
reconsider x9 = x as Element of L ;
consider y being Element of L such that
A7: y << x9 and
A8: y in X by A1, A5, A6, WAYBEL11:43;
set Y = uparrow y;
set bas =  {  (wayabove q) where q is Element of L : q << x9  }  ;
A9:  {  (wayabove q) where q is Element of L : q << x9  }  is Basis of x by A1, WAYBEL11:44;
 wayabove y in  {  (wayabove q) where q is Element of L : q << x9  }  by A7;
then  wayabove y is open by A9, YELLOW_8:12;
then A10: wayabove y c= Int (uparrow y) by TOPS_1:24, WAYBEL_3:11;
take  uparrow y ; ::_thesis: ( x in Int (uparrow y) & uparrow y c= X & uparrow y is compact )
 x in wayabove y by A7;
hence  x in Int (uparrow y) by A10; ::_thesis: ( uparrow y c= X & uparrow y is compact )
 X is upper by A6, WAYBEL11:def_4;
hence  uparrow y c= X by A8, WAYBEL11:42; ::_thesis: uparrow y is compact
thus  uparrow y is compact by A3, Th22; ::_thesis: verum
end;
 sup_op L is jointly_Scott-continuous by A1, Th30;
hence  L is sober by Th31; ::_thesis: L is Baire
hence  L is Baire by A4, WAYBEL12:44; ::_thesis: verum
end;

theorem Th33: :: WAYBEL14:33
for L being complete Scott TopLattice
for X being Subset of L st L is continuous & X in sigma L holds
X = union  {  (wayabove x) where x is Element of L : x in X  }
proof
let L be complete Scott TopLattice; ::_thesis: for X being Subset of L st L is continuous & X in sigma L holds
X = union  {  (wayabove x) where x is Element of L : x in X  }
let X be Subset of L; ::_thesis: ( L is continuous & X in sigma L implies X = union  {  (wayabove x) where x is Element of L : x in X  }  )
assume that
A1: L is continuous and
A2: X in sigma L ; ::_thesis: X = union  {  (wayabove x) where x is Element of L : x in X  }
set WAV =  {  (wayabove x) where x is Element of L : x in X  }  ;
A3: X is open by A2, Th24;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_x_in_union__{__(wayabove_x)_where_x_is_Element_of_L_:_x_in_X__}__)_&_(_x_in_union__{__(wayabove_x)_where_x_is_Element_of_L_:_x_in_X__}__implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies x in union  {  (wayabove x) where x is Element of L : x in X  }  ) & ( x in union  {  (wayabove x) where x is Element of L : x in X  }  implies x in X ) )
hereby  ::_thesis: ( x in union  {  (wayabove x) where x is Element of L : x in X  }  implies x in X )
assume A4: x in X ; ::_thesis: x in union  {  (wayabove x) where x is Element of L : x in X  }
then reconsider x9 = x as Element of L ;
consider q being Element of L such that
A5: ( q << x9 & q in X ) by A1, A3, A4, WAYBEL11:43;
 ( x9 in wayabove q & wayabove q in  {  (wayabove x) where x is Element of L : x in X  }  ) by A5;
hence  x in union  {  (wayabove x) where x is Element of L : x in X  }  by TARSKI:def_4; ::_thesis: verum
end;
assume  x in union  {  (wayabove x) where x is Element of L : x in X  }  ; ::_thesis: x in X
then consider Y being set  such that
A6: x in Y and
A7: Y in  {  (wayabove x) where x is Element of L : x in X  }  by TARSKI:def_4;
consider q being Element of L such that
A8: Y = wayabove q and
A9: q in X by A7;
A10: wayabove q c= uparrow q by WAYBEL_3:11;
 X is upper by A3, WAYBEL11:def_4;
then  uparrow q c= X by A9, WAYBEL11:42;
then  Y c= X by A8, A10, XBOOLE_1:1;
hence  x in X by A6; ::_thesis: verum
end;
hence  X = union  {  (wayabove x) where x is Element of L : x in X  }  by TARSKI:1; ::_thesis: verum
end;

theorem :: WAYBEL14:34
for L being complete Scott TopLattice st ( for X being Subset of L st X in sigma L holds
X = union  {  (wayabove x) where x is Element of L : x in X  }  ) holds
L is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for X being Subset of L st X in sigma L holds
X = union  {  (wayabove x) where x is Element of L : x in X  }  ) implies L is continuous )
assume A1: for X being Subset of L st X in sigma L holds
X = union  {  (wayabove x) where x is Element of L : x in X  }  ; ::_thesis: L is continuous
thus  for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus  L is up-complete ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L)
set y = sup (waybelow x);
set X = (downarrow (sup (waybelow x))) ` ;
assume A2: x <> sup (waybelow x) ; ::_thesis: contradiction
A3: sup (waybelow x) <= x by Th9;
now__::_thesis:_not_x_in_downarrow_(sup_(waybelow_x))
assume  x in downarrow (sup (waybelow x)) ; ::_thesis: contradiction
then  x <= sup (waybelow x) by WAYBEL_0:17;
hence  contradiction by A3, A2, ORDERS_2:2; ::_thesis: verum
end;
then A4: x in (downarrow (sup (waybelow x))) ` by XBOOLE_0:def_5;
set Z =  {  (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) `  }  ;
A5: sup (waybelow x) is_>=_than waybelow x by YELLOW_0:32;
 (downarrow (sup (waybelow x))) ` is open by WAYBEL11:12;
then  (downarrow (sup (waybelow x))) ` in sigma L by Th24;
then  (downarrow (sup (waybelow x))) ` = union  {  (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) `  }  by A1;
then consider Y being set  such that
A6: x in Y and
A7: Y in  {  (wayabove z) where z is Element of L : z in (downarrow (sup (waybelow x))) `  }  by A4, TARSKI:def_4;
consider z being Element of L such that
A8: Y = wayabove z and
A9: z in (downarrow (sup (waybelow x))) ` by A7;
 z << x by A6, A8, WAYBEL_3:8;
then  z in waybelow x ;
then  z <= sup (waybelow x) by A5, LATTICE3:def_9;
then  z in downarrow (sup (waybelow x)) by WAYBEL_0:17;
hence  contradiction by A9, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: WAYBEL14:35
for L being complete Scott TopLattice
for x being Element of L st L is continuous holds
ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L st L is continuous holds
ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
let x be Element of L; ::_thesis: ( L is continuous implies ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) )
set B =  {  V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered )  }  ;
  {  V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered )  }  c= bool the carrier of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered )  }  or X in bool the carrier of L )
assume  X in  {  V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered )  }  ; ::_thesis: X in bool the carrier of L
then  ex V being Subset of L st
( X = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence  X in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B =  {  V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered )  }  as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
assume A1: L is continuous ; ::_thesis: ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
then reconsider A =  {  (wayabove q) where q is Element of L : q << x  }  as Basis of x by WAYBEL11:44;
A2: B is Basis of x
proof
A3: B is open
proof
let Y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not Y in B or Y is open )
assume  Y in B ; ::_thesis: Y is open
then  ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence  Y is open ; ::_thesis: verum
end;
 B is x -quasi_basis
proof
thus  x in Intersect B :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in B & b2 c= b1 ) )
proof
percases ( B is empty or not B is empty ) ;
suppose B is empty ; ::_thesis: x in Intersect B
then  Intersect B = the carrier of L by SETFAM_1:def_9;
hence  x in Intersect B ; ::_thesis: verum
end;
supposeA4: not B is empty ; ::_thesis: x in Intersect B
A5: now__::_thesis:_for_Y_being_set_st_Y_in_B_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in B implies x in Y )
assume  Y in B ; ::_thesis: x in Y
then  ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence  x in Y ; ::_thesis: verum
end;
 Intersect B = meet B by A4, SETFAM_1:def_9;
hence  x in Intersect B by A4, A5, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S ) )
assume  ( S is open & x in S ) ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S )
then consider V being Subset of L such that
A6: V in A and
A7: V c= S by YELLOW_8:def_1;
consider q being Element of L such that
A8: V = wayabove q and
A9: q << x by A6;
consider F being Open Filter of L such that
A10: x in F and
A11: F c= wayabove q by A1, A9, WAYBEL_6:8;
take  F ; ::_thesis: ( F in B & F c= S )
 F is open by WAYBEL11:41;
hence  F in B by A9, A10, A11; ::_thesis: F c= S
thus  F c= S by A7, A8, A11, XBOOLE_1:1; ::_thesis: verum
end;
hence  B is Basis of x by A3; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_Subset_of_L_st_Y_in_B_holds_
(_Y_is_open_&_Y_is_filtered_)
let Y be Subset of L; ::_thesis: ( Y in B implies ( Y is open & Y is filtered ) )
assume  Y in B ; ::_thesis: ( Y is open & Y is filtered )
then  ex V being Subset of L st
( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence  ( Y is open & Y is filtered ) ; ::_thesis: verum
end;
hence  ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) by A2; ::_thesis: verum
end;

theorem :: WAYBEL14:36
for L being complete Scott TopLattice st L is continuous holds
InclPoset (sigma L) is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( L is continuous implies InclPoset (sigma L) is continuous )
assume A1: L is continuous ; ::_thesis: InclPoset (sigma L) is continuous
set IPs = InclPoset the topology of L;
A2: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
 InclPoset the topology of L is satisfying_axiom_of_approximation
proof
let V be Element of (InclPoset the topology of L); :: according to WAYBEL_3:def_5 ::_thesis: V = "\/" ((waybelow V),(InclPoset the topology of L))
set VV =  {  (wayabove x) where x is Element of L : x in V  }  ;
set wV = waybelow V;
 V in sigma L by A3, A2;
then A4: V = union  {  (wayabove x) where x is Element of L : x in V  }  by A1, Th33;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_V_implies_x_in_union_(waybelow_V)_)_&_(_x_in_union_(waybelow_V)_implies_x_in_V_)_)
let x be set ; ::_thesis: ( ( x in V implies x in union (waybelow V) ) & ( x in union (waybelow V) implies x in V ) )
hereby  ::_thesis: ( x in union (waybelow V) implies x in V )
assume  x in V ; ::_thesis: x in union (waybelow V)
then consider xU being set  such that
A5: x in xU and
A6: xU in  {  (wayabove x) where x is Element of L : x in V  }  by A4, TARSKI:def_4;
consider y being Element of L such that
A7: xU = wayabove y and
A8: y in V by A6;
 wayabove y is open by A1, WAYBEL11:36;
then reconsider xU = xU as Element of (InclPoset the topology of L) by A2, A7, PRE_TOPC:def_2;
 xU << V
proof
let D be non empty directed Subset of (InclPoset the topology of L); :: according to WAYBEL_3:def_1 ::_thesis: ( not V <= "\/" (D,(InclPoset the topology of L)) or ex b1 being Element of the carrier of (InclPoset the topology of L) st
( b1 in D & xU <= b1 ) )
assume  V <= sup D ; ::_thesis: ex b1 being Element of the carrier of (InclPoset the topology of L) st
( b1 in D & xU <= b1 )
then  V c= sup D by YELLOW_1:3;
then  V c= union D by YELLOW_1:22;
then consider DD being set  such that
A9: y in DD and
A10: DD in D by A8, TARSKI:def_4;
 DD in sigma L by A3, A2, A10;
then reconsider DD = DD as Subset of L ;
 DD is open by A2, A10, PRE_TOPC:def_2;
then  DD is upper by WAYBEL11:def_4;
then A11: uparrow y c= DD by A9, WAYBEL11:42;
reconsider d = DD as Element of (InclPoset the topology of L) by A10;
take  d ; ::_thesis: ( d in D & xU <= d )
thus  d in D by A10; ::_thesis: xU <= d
 wayabove y c= uparrow y by WAYBEL_3:11;
then  wayabove y c= DD by A11, XBOOLE_1:1;
hence  xU <= d by A7, YELLOW_1:3; ::_thesis: verum
end;
then  xU in waybelow V ;
hence  x in union (waybelow V) by A5, TARSKI:def_4; ::_thesis: verum
end;
assume  x in union (waybelow V) ; ::_thesis: x in V
then consider X being set  such that
A12: x in X and
A13: X in waybelow V by TARSKI:def_4;
reconsider X = X as Element of (InclPoset the topology of L) by A13;
 X << V by A13, WAYBEL_3:7;
then  X <= V by WAYBEL_3:1;
then  X c= V by YELLOW_1:3;
hence  x in V by A12; ::_thesis: verum
end;
then  V = union (waybelow V) by TARSKI:1;
hence  V = "\/" ((waybelow V),(InclPoset the topology of L)) by YELLOW_1:22; ::_thesis: verum
end;
hence  InclPoset (sigma L) is continuous by Th23; ::_thesis: verum
end;

theorem Th37: :: WAYBEL14:37
for L being complete Scott TopLattice
for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L)
proof
let L be complete Scott TopLattice; ::_thesis: for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L)
let x be Element of L; ::_thesis: ( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous implies x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L) )
assume that
A1: for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) and
A2: InclPoset (sigma L) is continuous ; ::_thesis: x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L)
A3: sigma L = the topology of L by Th23;
set IU =  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ;
set IPs = InclPoset the topology of L;
A4: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
set y = "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L);
set VVl = (downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L))) ` ;
now__::_thesis:_for_b_being_Element_of_L_st_b_in__{__(inf_V)_where_V_is_Subset_of_L_:_(_x_in_V_&_V_in_sigma_L_)__}__holds_
b_<=_x
let b be Element of L; ::_thesis: ( b in  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  implies b <= x )
assume  b in  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ; ::_thesis: b <= x
then consider V being Subset of L such that
A5: b = inf V and
A6: x in V and
 V in sigma L ;
 b is_<=_than V by A5, YELLOW_0:33;
hence  b <= x by A6, LATTICE3:def_8; ::_thesis: verum
end;
then  x is_>=_than  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  by LATTICE3:def_9;
then A7: "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) <= x by YELLOW_0:32;
assume A8: x <> "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) ; ::_thesis: contradiction
now__::_thesis:_not_x_in_downarrow_("\/"_(_{__(inf_V)_where_V_is_Subset_of_L_:_(_x_in_V_&_V_in_sigma_L_)__}__,L))
assume  x in downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L)) ; ::_thesis: contradiction
then  x <= "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) by WAYBEL_0:17;
hence  contradiction by A7, A8, ORDERS_2:2; ::_thesis: verum
end;
then A9: x in (downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L))) ` by XBOOLE_0:def_5;
 (downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L))) ` is open by WAYBEL11:12;
then reconsider VVp = (downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L))) ` as Element of (InclPoset the topology of L) by A3, A4, Th24;
 VVp = sup (waybelow VVp) by A2, A3, WAYBEL_3:def_5;
then  VVp = union (waybelow VVp) by YELLOW_1:22;
then consider Vp being set  such that
A10: x in Vp and
A11: Vp in waybelow VVp by A9, TARSKI:def_4;
reconsider Vp = Vp as Element of (InclPoset the topology of L) by A11;
 Vp in sigma L by A3, A4;
then reconsider Vl = Vp as Subset of L ;
A12: Vp << VVp by A11, WAYBEL_3:7;
consider bas being Basis of x such that
A13: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A1;
A14: "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) is_>=_than  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  by YELLOW_0:32;
 Vl is open by A4, PRE_TOPC:def_2;
then consider Ul being Subset of L such that
A15: Ul in bas and
A16: Ul c= Vl by A10, YELLOW_8:def_1;
set F =  {  (downarrow u) where u is Element of L : u in Ul  }  ;
A17: x in Ul by A15, YELLOW_8:12;
then A18: downarrow x in  {  (downarrow u) where u is Element of L : u in Ul  }  ;
  {  (downarrow u) where u is Element of L : u in Ul  }  c= bool the carrier of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  (downarrow u) where u is Element of L : u in Ul  }  or X in bool the carrier of L )
assume  X in  {  (downarrow u) where u is Element of L : u in Ul  }  ; ::_thesis: X in bool the carrier of L
then  ex u being Element of L st
( X = downarrow u & u in Ul ) ;
hence  X in bool the carrier of L ; ::_thesis: verum
end;
then reconsider F =  {  (downarrow u) where u is Element of L : u in Ul  }  as non empty Subset-Family of L by A18;
 COMPLEMENT F c= the topology of L
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in COMPLEMENT F or X in the topology of L )
assume A19: X in COMPLEMENT F ; ::_thesis: X in the topology of L
then reconsider X9 = X as Subset of L ;
 X9 ` in F by A19, SETFAM_1:def_7;
then consider u being Element of L such that
A20: X9 ` = downarrow u and
 u in Ul ;
 X9 = (downarrow u) ` by A20;
then  X9 is open by WAYBEL11:12;
hence  X in the topology of L by PRE_TOPC:def_2; ::_thesis: verum
end;
then reconsider CF = COMPLEMENT F as Subset of (InclPoset the topology of L) by YELLOW_1:1;
 Ul is filtered by A13, A15;
then A21: CF is directed by A3, Lm2;
 Ul is open by A15, YELLOW_8:12;
then  Ul in sigma L by A3, PRE_TOPC:def_2;
then  inf Ul in  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  by A17;
then  inf Ul <= "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) by A14, LATTICE3:def_9;
then  downarrow (inf Ul) c= downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L)) by WAYBEL_0:21;
then A22: (downarrow ("\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L))) ` c= (downarrow (inf Ul)) ` by SUBSET_1:12;
 downarrow (inf Ul) = meet F by A17, Th15;
then  (downarrow (inf Ul)) ` = union (COMPLEMENT F) by TOPS_2:7;
then  VVp c= sup CF by A22, YELLOW_1:22;
then A23: VVp <= sup CF by YELLOW_1:3;
 (downarrow x) ` in COMPLEMENT F by A18, YELLOW_8:5;
then consider d being Element of (InclPoset the topology of L) such that
A24: d in CF and
A25: Vp << d by A2, A3, A12, A21, A23, WAYBEL_4:53;
 Vp <= d by A25, WAYBEL_3:1;
then A26: Vp c= d by YELLOW_1:3;
 d in sigma L by A3, A4;
then reconsider d9 = d as Subset of L ;
 d9 ` in F by A24, SETFAM_1:def_7;
then consider u being Element of L such that
A27: d9 ` = downarrow u and
A28: u in Ul ;
 u <= u ;
then  u in downarrow u by WAYBEL_0:17;
then  not u in Vp by A27, A26, XBOOLE_0:def_5;
hence  contradiction by A16, A28; ::_thesis: verum
end;

theorem Th38: :: WAYBEL14:38
for L being complete Scott TopLattice st ( for x being Element of L holds x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L) ) holds
L is continuous
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for x being Element of L holds x = "\/" ( {  (inf X) where X is Subset of L : ( x in X & X in sigma L )  }  ,L) ) implies L is continuous )
assume A1: for x being Element of L holds x = "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) ; ::_thesis: L is continuous
thus  for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def_6 ::_thesis: ( L is up-complete & L is satisfying_axiom_of_approximation )
thus  L is up-complete ; ::_thesis: L is satisfying_axiom_of_approximation
let x be Element of L; :: according to WAYBEL_3:def_5 ::_thesis: x = "\/" ((waybelow x),L)
set VV =  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ;
A2: sup (waybelow x) <= x by Th9;
A3:  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  c= waybelow x
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  or d in waybelow x )
assume  d in  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ; ::_thesis: d in waybelow x
then consider V being Subset of L such that
A4: inf V = d and
A5: x in V and
A6: V in sigma L ;
 V is open by A6, Th24;
then  inf V << x by A5, Th26;
hence  d in waybelow x by A4; ::_thesis: verum
end;
 ( ex_sup_of  {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L & ex_sup_of waybelow x,L ) by YELLOW_0:17;
then A7: "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) <= sup (waybelow x) by A3, YELLOW_0:34;
 x = "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) by A1;
hence  x = "\/" ((waybelow x),L) by A7, A2, ORDERS_2:2; ::_thesis: verum
end;

theorem Th39: :: WAYBEL14:39
for L being complete Scott TopLattice holds
( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) iff for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) )
set IPs = InclPoset the topology of L;
A1: sigma L = the topology of L by Th23;
then A2: the carrier of (InclPoset the topology of L) = sigma L by YELLOW_1:1;
hereby  ::_thesis: ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) implies for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) )
assume A3: for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ; ::_thesis: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
let V be Element of (InclPoset (sigma L)); ::_thesis: ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
set X =  {  Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) )  }  ;
now__::_thesis:_for_YY_being_set_st_YY_in__{__Y_where_Y_is_Subset_of_L_:_(_Y_c=_V_&_ex_x_being_Element_of_L_ex_bas_being_Basis_of_x_st_
(_x_in_V_&_Y_in_bas_&_(_for_Yx_being_Subset_of_L_st_Yx_in_bas_holds_
(_Yx_is_open_&_Yx_is_filtered_)_)_)_)__}__holds_
YY_in_the_carrier_of_(InclPoset_(sigma_L))
let YY be set ; ::_thesis: ( YY in  {  Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) )  }  implies YY in the carrier of (InclPoset (sigma L)) )
assume  YY in  {  Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) )  }  ; ::_thesis: YY in the carrier of (InclPoset (sigma L))
then consider Y being Subset of L such that
A4: Y = YY and
 Y c= V and
A5: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
 Y is open by A5;
then  Y in sigma L by Th24;
hence  YY in the carrier of (InclPoset (sigma L)) by A4, YELLOW_1:1; ::_thesis: verum
end;
then reconsider X =  {  Y where Y is Subset of L : ( Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) )  }  as Subset of (InclPoset (sigma L)) by TARSKI:def_3;
take X = X; ::_thesis: ( V = sup X & ( for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime ) )
 V in sigma L by A1, A2;
then reconsider Vl = V as Subset of L ;
A6: Vl is open by A1, A2, Th24;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_V_implies_x_in_union_X_)_&_(_x_in_union_X_implies_x_in_V_)_)
let x be set ; ::_thesis: ( ( x in V implies x in union X ) & ( x in union X implies x in V ) )
hereby  ::_thesis: ( x in union X implies x in V )
assume A7: x in V ; ::_thesis: x in union X
 Vl = V ;
then reconsider d = x as Element of L by A7;
consider bas being Basis of d such that
A8: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A3;
consider Y being Subset of L such that
A9: Y in bas and
A10: Y c= V by A6, A7, YELLOW_8:13;
A11: x in Y by A9, YELLOW_8:12;
 Y in X by A7, A8, A9, A10;
hence  x in union X by A11, TARSKI:def_4; ::_thesis: verum
end;
assume  x in union X ; ::_thesis: x in V
then consider YY being set  such that
A12: x in YY and
A13: YY in X by TARSKI:def_4;
 ex Y being Subset of L st
( Y = YY & Y c= V & ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ) by A13;
hence  x in V by A12; ::_thesis: verum
end;
then  V = union X by TARSKI:1;
hence  V = sup X by A1, YELLOW_1:22; ::_thesis: for Yp being Element of (InclPoset (sigma L)) st Yp in X holds
Yp is co-prime
let Yp be Element of (InclPoset (sigma L)); ::_thesis: ( Yp in X implies Yp is co-prime )
assume  Yp in X ; ::_thesis: Yp is co-prime
then consider Y being Subset of L such that
A14: Y = Yp and
 Y c= V and
A15: ex x being Element of L ex bas being Basis of x st
( x in V & Y in bas & ( for Yx being Subset of L st Yx in bas holds
( Yx is open & Yx is filtered ) ) ) ;
A16: ( Y is open & Y is filtered ) by A15;
then  Y is upper by WAYBEL11:def_4;
hence  Yp is co-prime by A14, A16, Th27; ::_thesis: verum
end;
assume A17: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; ::_thesis: for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered )
let x be Element of L; ::_thesis: ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered )
set bas =  {  V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime )  }  ;
  {  V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime )  }  c= bool the carrier of L
proof
let VV be set ; :: according to TARSKI:def_3 ::_thesis: ( not VV in  {  V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime )  }  or VV in bool the carrier of L )
assume  VV in  {  V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime )  }  ; ::_thesis: VV in bool the carrier of L
then  ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
then  VV in sigma L by A1, A2;
hence  VV in bool the carrier of L ; ::_thesis: verum
end;
then reconsider bas =  {  V where V is Element of (InclPoset (sigma L)) : ( x in V & V is co-prime )  }  as Subset-Family of L ;
reconsider bas = bas as Subset-Family of L ;
 bas is Basis of x
proof
A18: bas is open
proof
let VV be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not VV in bas or VV is open )
assume  VV in bas ; ::_thesis: VV is open
then  ex V being Element of (InclPoset (sigma L)) st
( VV = V & x in V & V is co-prime ) ;
hence  VV is open by A1, A2, PRE_TOPC:def_2; ::_thesis: verum
end;
 bas is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_bas
percases ( bas is empty or not bas is empty ) ;
suppose bas is empty ; ::_thesis: x in Intersect bas
then  Intersect bas = the carrier of L by SETFAM_1:def_9;
hence  x in Intersect bas ; ::_thesis: verum
end;
supposeA19: not bas is empty ; ::_thesis: x in Intersect bas
A20: now__::_thesis:_for_Y_being_set_st_Y_in_bas_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in bas implies x in Y )
assume  Y in bas ; ::_thesis: x in Y
then  ex V being Element of (InclPoset (sigma L)) st
( Y = V & x in V & V is co-prime ) ;
hence  x in Y ; ::_thesis: verum
end;
 Intersect bas = meet bas by A19, SETFAM_1:def_9;
hence  x in Intersect bas by A19, A20, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in Intersect bas ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in bas & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in bas & b1 c= S ) )
assume that
A21: S is open and
A22: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in bas & b1 c= S )
reconsider S9 = S as Element of (InclPoset the topology of L) by A2, A21, Th24;
consider X being Subset of (InclPoset the topology of L) such that
A23: S9 = sup X and
A24: for x being Element of (InclPoset the topology of L) st x in X holds
x is co-prime by A1, A17;
 S9 = union X by A23, YELLOW_1:22;
then consider V being set  such that
A25: x in V and
A26: V in X by A22, TARSKI:def_4;
 V in sigma L by A2, A26;
then reconsider V = V as Subset of L ;
reconsider Vp = V as Element of (InclPoset the topology of L) by A26;
take  V ; ::_thesis: ( V in bas & V c= S )
 Vp is co-prime by A24, A26;
hence  V in bas by A1, A25; ::_thesis: V c= S
 sup X is_>=_than X by YELLOW_0:32;
then  Vp <= sup X by A26, LATTICE3:def_9;
hence  V c= S by A23, YELLOW_1:3; ::_thesis: verum
end;
hence  bas is Basis of x by A18; ::_thesis: verum
end;
then reconsider bas = bas as Basis of x ;
take  bas ; ::_thesis: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered )
let V be Subset of L; ::_thesis: ( V in bas implies ( V is open & V is filtered ) )
assume  V in bas ; ::_thesis: ( V is open & V is filtered )
then  ex Vp being Element of (InclPoset (sigma L)) st
( V = Vp & x in Vp & Vp is co-prime ) ;
hence  ( V is open & V is filtered ) by A1, A2, Th24, Th27; ::_thesis: verum
end;

theorem :: WAYBEL14:40
for L being complete Scott TopLattice holds
( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )
proof
let L be complete Scott TopLattice; ::_thesis: ( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive )
 InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence  ( ( ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) & InclPoset (sigma L) is continuous ) iff InclPoset (sigma L) is completely-distributive ) by WAYBEL_6:38; ::_thesis: verum
end;

theorem :: WAYBEL14:41
for L being complete Scott TopLattice holds
( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) )
 InclPoset (sigma L) = InclPoset the topology of L by Th23;
hence  ( InclPoset (sigma L) is completely-distributive iff ( InclPoset (sigma L) is continuous & (InclPoset (sigma L)) opp is continuous ) ) by WAYBEL_6:39; ::_thesis: verum
end;

theorem :: WAYBEL14:42
for L being complete Scott TopLattice st L is algebraic holds
ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }
proof
let L be complete Scott TopLattice; ::_thesis: ( L is algebraic implies ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  )
set P =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ;
  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  or x in bool the carrier of L )
assume  x in  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ; ::_thesis: x in bool the carrier of L
then  ex k being Element of L st
( x = uparrow k & k in the carrier of (CompactSublatt L) ) ;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider P =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  as Subset-Family of L ;
reconsider P = P as Subset-Family of L ;
A1: P c= the topology of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in the topology of L )
assume  x in P ; ::_thesis: x in the topology of L
then consider k being Element of L such that
A2: x = uparrow k and
A3: k in the carrier of (CompactSublatt L) ;
 k is compact by A3, WAYBEL_8:def_1;
then  uparrow k is Open by WAYBEL_8:2;
then  uparrow k is open by WAYBEL11:41;
hence  x in the topology of L by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
assume A4: L is algebraic ; ::_thesis: ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }
now__::_thesis:_for_x_being_Point_of_L_ex_B_being_Basis_of_x_st_B_c=_P
let x be Point of L; ::_thesis: ex B being Basis of x st B c= P
set B =  {  (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k )  }  ;
  {  (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k )  }  c= bool the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k )  }  or y in bool the carrier of L )
assume  y in  {  (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k )  }  ; ::_thesis: y in bool the carrier of L
then  ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence  y in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B =  {  (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k )  }  as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
 B is Basis of x
proof
A5: B is open
proof
let y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not y in B or y is open )
assume  y in B ; ::_thesis: y is open
then  ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence  y is open by A1, PRE_TOPC:def_2; ::_thesis: verum
end;
 B is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_B
percases ( B is empty or not B is empty ) ;
suppose B is empty ; ::_thesis: x in Intersect B
then  Intersect B = the carrier of L by SETFAM_1:def_9;
hence  x in Intersect B ; ::_thesis: verum
end;
supposeA6: not B is empty ; ::_thesis: x in Intersect B
A7: now__::_thesis:_for_Y_being_set_st_Y_in_B_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in B implies x in Y )
assume  Y in B ; ::_thesis: x in Y
then  ex k being Element of L st
( Y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence  x in Y ; ::_thesis: verum
end;
 Intersect B = meet B by A6, SETFAM_1:def_9;
hence  x in Intersect B by A6, A7, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in Intersect B ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in B & b2 c= b1 ) )
reconsider x9 = x as Element of L ;
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S ) )
assume that
A8: S is open and
A9: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in B & b1 c= S )
A10: x = sup (compactbelow x9) by A4, WAYBEL_8:def_3;
 S is inaccessible by A8, WAYBEL11:def_4;
then  compactbelow x9 meets S by A9, A10, WAYBEL11:def_1;
then consider k being set  such that
A11: k in compactbelow x9 and
A12: k in S by XBOOLE_0:3;
reconsider k = k as Element of L by A11;
A13: compactbelow x9 = (downarrow x9) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
then  k in downarrow x9 by A11, XBOOLE_0:def_4;
then  k <= x9 by WAYBEL_0:17;
then A14: x in uparrow k by WAYBEL_0:18;
take V = uparrow k; ::_thesis: ( V in B & V c= S )
 k in the carrier of (CompactSublatt L) by A11, A13, XBOOLE_0:def_4;
then  uparrow k in P ;
hence  V in B by A14; ::_thesis: V c= S
 S is upper by A8, WAYBEL11:def_4;
hence  V c= S by A12, WAYBEL11:42; ::_thesis: verum
end;
hence  B is Basis of x by A5; ::_thesis: verum
end;
then reconsider B = B as Basis of x ;
take B = B; ::_thesis: B c= P
thus  B c= P ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B or y in P )
assume  y in B ; ::_thesis: y in P
then  ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence  y in P ; ::_thesis: verum
end;
end;
then  P is Basis of L by A1, YELLOW_8:14;
hence  ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  ; ::_thesis: verum
end;

theorem :: WAYBEL14:43
for L being complete Scott TopLattice st ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  holds
( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) )
proof
let L be complete Scott TopLattice; ::_thesis: ( ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  implies ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) ) )
given B being Basis of L such that A1: B =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ; ::_thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) )
set IPs = InclPoset (sigma L);
set IPt = InclPoset the topology of L;
A2: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
A4: InclPoset (sigma L) = InclPoset the topology of L by Th23;
thus  InclPoset (sigma L) is algebraic ::_thesis: for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) )
proof
thus  for X being Element of (InclPoset (sigma L)) holds
( not compactbelow X is empty & compactbelow X is directed ) by A3; :: according to WAYBEL_8:def_4 ::_thesis: ( InclPoset (sigma L) is up-complete & InclPoset (sigma L) is satisfying_axiom_K )
thus  InclPoset (sigma L) is up-complete by A4; ::_thesis: InclPoset (sigma L) is satisfying_axiom_K
let X be Element of (InclPoset (sigma L)); :: according to WAYBEL_8:def_3 ::_thesis: X = "\/" ((compactbelow X),(InclPoset (sigma L)))
set cX = compactbelow X;
set GB =  {  G where G is Subset of L : ( G in B & G c= X )  }  ;
 X in sigma L by A2;
then reconsider X9 = X as Subset of L ;
 X9 is open by A2, Th24;
then A5: X = union  {  G where G is Subset of L : ( G in B & G c= X )  }  by YELLOW_8:9;
A6: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_X_implies_x_in_union_(compactbelow_X)_)_&_(_x_in_union_(compactbelow_X)_implies_x_in_X_)_)
let x be set ; ::_thesis: ( ( x in X implies x in union (compactbelow X) ) & ( x in union (compactbelow X) implies x in X ) )
hereby  ::_thesis: ( x in union (compactbelow X) implies x in X )
assume  x in X ; ::_thesis: x in union (compactbelow X)
then consider GG being set  such that
A7: x in GG and
A8: GG in  {  G where G is Subset of L : ( G in B & G c= X )  }  by A5, TARSKI:def_4;
consider G being Subset of L such that
A9: G = GG and
A10: G in B and
A11: G c= X by A8;
consider k being Element of L such that
A12: G = uparrow k and
A13: k in the carrier of (CompactSublatt L) by A1, A10;
 k is compact by A13, WAYBEL_8:def_1;
then  uparrow k is Open by WAYBEL_8:2;
then  uparrow k is open by WAYBEL11:41;
then reconsider G = G as Element of (InclPoset (sigma L)) by A3, A2, A12, PRE_TOPC:def_2;
 for X being Subset of L st X is open holds
X is upper by WAYBEL11:def_4;
then  uparrow k is compact by Th22;
then A14: G is compact by A3, A12, WAYBEL_3:36;
 G <= X by A11, YELLOW_1:3;
then  G in compactbelow X by A14;
hence  x in union (compactbelow X) by A7, A9, TARSKI:def_4; ::_thesis: verum
end;
assume  x in union (compactbelow X) ; ::_thesis: x in X
then consider G being set  such that
A15: x in G and
A16: G in compactbelow X by TARSKI:def_4;
reconsider G = G as Element of (InclPoset (sigma L)) by A16;
 G <= X by A16, WAYBEL_8:4;
then  G c= X by YELLOW_1:3;
hence  x in X by A15; ::_thesis: verum
end;
 sup (compactbelow X) = union (compactbelow X) by A3, YELLOW_1:22;
hence  X = "\/" ((compactbelow X),(InclPoset (sigma L))) by A6, TARSKI:1; ::_thesis: verum
end;
let V be Element of (InclPoset (sigma L)); ::_thesis: ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) )
 V in sigma L by A2;
then reconsider V9 = V as Subset of L ;
set GB =  {  G where G is Subset of L : ( G in B & G c= V )  }  ;
  {  G where G is Subset of L : ( G in B & G c= V )  }  c= the carrier of (InclPoset (sigma L))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  G where G is Subset of L : ( G in B & G c= V )  }  or x in the carrier of (InclPoset (sigma L)) )
assume  x in  {  G where G is Subset of L : ( G in B & G c= V )  }  ; ::_thesis: x in the carrier of (InclPoset (sigma L))
then consider G being Subset of L such that
A17: G = x and
A18: G in B and
 G c= V ;
 G is open by A18, YELLOW_8:10;
hence  x in the carrier of (InclPoset (sigma L)) by A2, A17, Th24; ::_thesis: verum
end;
then reconsider GB =  {  G where G is Subset of L : ( G in B & G c= V )  }  as Subset of (InclPoset (sigma L)) ;
take  GB ; ::_thesis: ( V = sup GB & ( for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime ) )
 V9 is open by A2, Th24;
then  V = union GB by YELLOW_8:9;
hence  V = sup GB by A3, YELLOW_1:22; ::_thesis: for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime
let x be Element of (InclPoset (sigma L)); ::_thesis: ( x in GB implies x is co-prime )
assume  x in GB ; ::_thesis: x is co-prime
then consider G being Subset of L such that
A19: G = x and
A20: G in B and
 G c= V ;
 ex k being Element of L st
( G = uparrow k & k in the carrier of (CompactSublatt L) ) by A1, A20;
hence  x is co-prime by A19, Th27; ::_thesis: verum
end;

theorem :: WAYBEL14:44
for L being complete Scott TopLattice st InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) holds
ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }
proof
let L be complete Scott TopLattice; ::_thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) implies ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  )
set IPt = InclPoset the topology of L;
set IPs = InclPoset (sigma L);
A1: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
set B =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ;
  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  c= bool the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  or x in bool the carrier of L )
assume  x in  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ; ::_thesis: x in bool the carrier of L
then  ex k being Element of L st
( x = uparrow k & k in the carrier of (CompactSublatt L) ) ;
hence  x in bool the carrier of L ; ::_thesis: verum
end;
then reconsider B =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  as Subset-Family of L ;
assume that
A2: InclPoset (sigma L) is algebraic and
A3: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; ::_thesis: ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }
 InclPoset (sigma L) = InclPoset the topology of L by Th23;
then reconsider ips = InclPoset (sigma L) as algebraic LATTICE by A2;
reconsider B = B as Subset-Family of L ;
A4: B c= the topology of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B or x in the topology of L )
assume  x in B ; ::_thesis: x in the topology of L
then consider k being Element of L such that
A5: x = uparrow k and
A6: k in the carrier of (CompactSublatt L) ;
 k is compact by A6, WAYBEL_8:def_1;
then  uparrow k is Open by WAYBEL_8:2;
then  uparrow k is open by WAYBEL11:41;
hence  x in the topology of L by A5, PRE_TOPC:def_2; ::_thesis: verum
end;
A7: sigma L = the topology of L by Th23;
 ( ips is continuous & ( for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ) ) by A3, Th39;
then  for x being Element of L holds x = "\/" ( {  (inf V) where V is Subset of L : ( x in V & V in sigma L )  }  ,L) by Th37;
then A8: L is continuous by Th38;
now__::_thesis:_for_x_being_Point_of_L_ex_Bx_being_Basis_of_x_st_Bx_c=_B
let x be Point of L; ::_thesis: ex Bx being Basis of x st Bx c= B
set Bx =  {  (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k )  }  ;
  {  (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k )  }  c= bool the carrier of L
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k )  }  or y in bool the carrier of L )
assume  y in  {  (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k )  }  ; ::_thesis: y in bool the carrier of L
then  ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence  y in bool the carrier of L ; ::_thesis: verum
end;
then reconsider Bx =  {  (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k )  }  as Subset-Family of L ;
reconsider Bx = Bx as Subset-Family of L ;
 Bx is Basis of x
proof
A9: Bx is open
proof
let y be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not y in Bx or y is open )
assume  y in Bx ; ::_thesis: y is open
then  ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence  y is open by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
 Bx is x -quasi_basis
proof
now__::_thesis:_x_in_Intersect_Bx
percases ( Bx is empty or not Bx is empty ) ;
suppose Bx is empty ; ::_thesis: x in Intersect Bx
then  Intersect Bx = the carrier of L by SETFAM_1:def_9;
hence  x in Intersect Bx ; ::_thesis: verum
end;
supposeA10: not Bx is empty ; ::_thesis: x in Intersect Bx
A11: now__::_thesis:_for_Y_being_set_st_Y_in_Bx_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in Bx implies x in Y )
assume  Y in Bx ; ::_thesis: x in Y
then  ex k being Element of L st
( Y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence  x in Y ; ::_thesis: verum
end;
 Intersect Bx = meet Bx by A10, SETFAM_1:def_9;
hence  x in Intersect Bx by A10, A11, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
hence  x in Intersect Bx ; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of bool the carrier of L holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of L st
( b2 in Bx & b2 c= b1 ) )
let S be Subset of L; ::_thesis: ( not S is open or not x in S or ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S ) )
assume that
A12: S is open and
A13: x in S ; ::_thesis: ex b1 being Element of bool the carrier of L st
( b1 in Bx & b1 c= S )
reconsider S9 = S as Element of (InclPoset the topology of L) by A7, A1, A12, PRE_TOPC:def_2;
 S9 = sup (compactbelow S9) by A2, A7, WAYBEL_8:def_3;
then  S9 = union (compactbelow S9) by YELLOW_1:22;
then consider UA being set  such that
A14: x in UA and
A15: UA in compactbelow S9 by A13, TARSKI:def_4;
reconsider UA = UA as Element of (InclPoset the topology of L) by A15;
 UA is compact by A15, WAYBEL_8:4;
then A16: UA << UA by WAYBEL_3:def_2;
 UA in the topology of L by A7, A1;
then reconsider UA9 = UA as Subset of L ;
 UA <= S9 by A15, WAYBEL_8:4;
then A17: UA c= S by YELLOW_1:3;
consider F being Subset of (InclPoset (sigma L)) such that
A18: UA = sup F and
A19: for x being Element of (InclPoset (sigma L)) st x in F holds
x is co-prime by A3, A7;
reconsider F9 = F as Subset-Family of L by A1, XBOOLE_1:1;
A20: UA = union F by A7, A18, YELLOW_1:22;
 F9 is open
proof
let P be Subset of L; :: according to TOPS_2:def_1 ::_thesis: ( not P in F9 or P is open )
assume  P in F9 ; ::_thesis: P is open
hence  P is open by A7, A1, PRE_TOPC:def_2; ::_thesis: verum
end;
then consider G being finite Subset of F9 such that
A21: UA c= union G by A20, A16, WAYBEL_3:34;
 union G c= union F by ZFMISC_1:77;
then A22: UA = union G by A20, A21, XBOOLE_0:def_10;
reconsider G = G as finite Subset-Family of L by XBOOLE_1:1;
consider Gg being finite Subset-Family of L such that
A23: Gg c= G and
A24: union Gg = union G and
A25: for g being Subset of L st g in Gg holds
not g c= union (Gg \ {g}) by Th1;
consider U1 being set  such that
A26: x in U1 and
A27: U1 in Gg by A14, A21, A24, TARSKI:def_4;
A28: Gg c= F by A23, XBOOLE_1:1;
then  U1 in F by A27;
then reconsider U1 = U1 as Element of (InclPoset (sigma L)) ;
 U1 in the topology of L by A7, A1;
then reconsider U19 = U1 as Subset of L ;
set k = inf U19;
A29: U19 c= uparrow (inf U19)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U19 or x in uparrow (inf U19) )
assume A30: x in U19 ; ::_thesis: x in uparrow (inf U19)
then reconsider x9 = x as Element of L ;
 inf U19 is_<=_than U19 by YELLOW_0:33;
then  inf U19 <= x9 by A30, LATTICE3:def_8;
hence  x in uparrow (inf U19) by WAYBEL_0:18; ::_thesis: verum
end;
 U1 is co-prime by A19, A27, A28;
then A31: ( U19 is filtered & U19 is upper ) by Th27;
now__::_thesis:_inf_U19_in_U19
set D =  {  ((downarrow u) `) where u is Element of L : u in U19  }  ;
A32:  {  ((downarrow u) `) where u is Element of L : u in U19  }  c= the topology of L
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in  {  ((downarrow u) `) where u is Element of L : u in U19  }  or d in the topology of L )
assume  d in  {  ((downarrow u) `) where u is Element of L : u in U19  }  ; ::_thesis: d in the topology of L
then consider u being Element of L such that
A33: d = (downarrow u) ` and
 u in U19 ;
 (downarrow u) ` is open by WAYBEL11:12;
hence  d in the topology of L by A33, PRE_TOPC:def_2; ::_thesis: verum
end;
consider u being set  such that
A34: u in U19 by A26;
reconsider u = u as Element of L by A34;
 (downarrow u) ` in  {  ((downarrow u) `) where u is Element of L : u in U19  }  by A34;
then reconsider D =  {  ((downarrow u) `) where u is Element of L : u in U19  }  as non empty Subset of (InclPoset the topology of L) by A32, YELLOW_1:1;
assume A35: not inf U19 in U19 ; ::_thesis: contradiction
now__::_thesis:_UA_c=_union_D
assume  not UA c= union D ; ::_thesis: contradiction
then consider l being set  such that
A36: l in UA9 and
A37: not l in union D by TARSKI:def_3;
reconsider l = l as Element of L by A36;
consider Uk being set  such that
A38: l in Uk and
A39: Uk in Gg by A21, A24, A36, TARSKI:def_4;
A40: Gg c= F by A23, XBOOLE_1:1;
then  Uk in F by A39;
then reconsider Uk = Uk as Element of (InclPoset (sigma L)) ;
 Uk in the topology of L by A7, A1;
then reconsider Uk9 = Uk as Subset of L ;
 Uk is co-prime by A19, A39, A40;
then A41: ( Uk9 is filtered & Uk9 is upper ) by Th27;
now__::_thesis:_l_is_<=_than_U19
assume  not l is_<=_than U19 ; ::_thesis: contradiction
then consider m being Element of L such that
A42: m in U19 and
A43: not l <= m by LATTICE3:def_8;
 (downarrow m) ` in D by A42;
then  not l in (downarrow m) ` by A37, TARSKI:def_4;
then  l in downarrow m by XBOOLE_0:def_5;
hence  contradiction by A43, WAYBEL_0:17; ::_thesis: verum
end;
then  l <= inf U19 by YELLOW_0:33;
then A44: inf U19 in Uk9 by A38, A41, WAYBEL_0:def_20;
A45: inf U19 is_<=_than U19 by YELLOW_0:33;
A46: U19 c= Uk
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in U19 or u in Uk )
assume A47: u in U19 ; ::_thesis: u in Uk
then reconsider d = u as Element of L ;
 inf U19 <= d by A45, A47, LATTICE3:def_8;
hence  u in Uk by A41, A44, WAYBEL_0:def_20; ::_thesis: verum
end;
 U19 c= union (Gg \ {U19})
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in U19 or u in union (Gg \ {U19}) )
assume A48: u in U19 ; ::_thesis: u in union (Gg \ {U19})
 Uk in Gg \ {U19} by A35, A39, A44, ZFMISC_1:56;
hence  u in union (Gg \ {U19}) by A46, A48, TARSKI:def_4; ::_thesis: verum
end;
hence  contradiction by A25, A27; ::_thesis: verum
end;
then  UA c= sup D by YELLOW_1:22;
then A49: UA <= sup D by YELLOW_1:3;
 D is directed by A7, A31, Th25;
then consider d being Element of (InclPoset the topology of L) such that
A50: d in D and
A51: UA <= d by A16, A49, WAYBEL_3:def_1;
consider u being Element of L such that
A52: d = (downarrow u) ` and
A53: u in U19 by A50;
 U1 c= UA by A20, A27, A28, ZFMISC_1:74;
then A54: u in UA by A53;
A55: u <= u ;
 UA c= d by A51, YELLOW_1:3;
then  not u in downarrow u by A52, A54, XBOOLE_0:def_5;
hence  contradiction by A55, WAYBEL_0:17; ::_thesis: verum
end;
then  uparrow (inf U19) c= U19 by A31, WAYBEL11:42;
then A56: U19 = uparrow (inf U19) by A29, XBOOLE_0:def_10;
take V = uparrow (inf U19); ::_thesis: ( V in Bx & V c= S )
 U19 is open by A7, A1, PRE_TOPC:def_2;
then  U19 is Open by A8, A31, WAYBEL11:46;
then  inf U19 is compact by A56, WAYBEL_8:2;
then  inf U19 in the carrier of (CompactSublatt L) by WAYBEL_8:def_1;
then  uparrow (inf U19) in B ;
hence  V in Bx by A26, A29; ::_thesis: V c= S
 U1 c= UA by A22, A24, A27, ZFMISC_1:74;
hence  V c= S by A56, A17, XBOOLE_1:1; ::_thesis: verum
end;
hence  Bx is Basis of x by A9; ::_thesis: verum
end;
then reconsider Bx = Bx as Basis of x ;
take Bx = Bx; ::_thesis: Bx c= B
thus  Bx c= B ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Bx or y in B )
assume  y in Bx ; ::_thesis: y in B
then  ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence  y in B ; ::_thesis: verum
end;
end;
then reconsider B = B as Basis of L by A4, YELLOW_8:14;
take  B ; ::_thesis: B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }
thus  B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  ; ::_thesis: verum
end;

theorem :: WAYBEL14:45
for L being complete Scott TopLattice st ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  holds
L is algebraic
proof
let L be complete Scott TopLattice; ::_thesis: ( ex B being Basis of L st B =  {  (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L)  }  implies L is algebraic )
given B being Basis of L such that A1: B =  {  (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L)  }  ; ::_thesis: L is algebraic
thus  for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def_4 ::_thesis: ( L is up-complete & L is satisfying_axiom_K )
thus  L is up-complete ; ::_thesis: L is satisfying_axiom_K
let x be Element of L; :: according to WAYBEL_8:def_3 ::_thesis: x = "\/" ((compactbelow x),L)
set y = sup (compactbelow x);
set cx = compactbelow x;
set dx = downarrow x;
set dy = downarrow (sup (compactbelow x));
now__::_thesis:_not_sup_(compactbelow_x)_<>_x
 for z being Element of L st z in downarrow x holds
z <= x by WAYBEL_0:17;
then  x is_>=_than downarrow x by LATTICE3:def_9;
then A2: sup (downarrow x) <= x by YELLOW_0:32;
set GB =  {  G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` )  }  ;
A3: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
A4: sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
 ( ex_sup_of compactbelow x,L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
then  sup (compactbelow x) <= sup (downarrow x) by A3, XBOOLE_1:17, YELLOW_0:34;
then A5: sup (compactbelow x) <= x by A2, ORDERS_2:3;
assume A6: sup (compactbelow x) <> x ; ::_thesis: contradiction
now__::_thesis:_not_x_in_downarrow_(sup_(compactbelow_x))
assume  x in downarrow (sup (compactbelow x)) ; ::_thesis: contradiction
then  x <= sup (compactbelow x) by WAYBEL_0:17;
hence  contradiction by A6, A5, ORDERS_2:2; ::_thesis: verum
end;
then A7: x in (downarrow (sup (compactbelow x))) ` by XBOOLE_0:def_5;
 (downarrow (sup (compactbelow x))) ` = union  {  G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` )  }  by WAYBEL11:12, YELLOW_8:9;
then consider X being set  such that
A8: x in X and
A9: X in  {  G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` )  }  by A7, TARSKI:def_4;
consider G being Subset of L such that
A10: G = X and
A11: G in B and
A12: G c= (downarrow (sup (compactbelow x))) ` by A9;
consider k being Element of L such that
A13: G = uparrow k and
A14: k in the carrier of (CompactSublatt L) by A1, A11;
A15: k is compact by A14, WAYBEL_8:def_1;
 k <= x by A8, A10, A13, WAYBEL_0:18;
then  k in compactbelow x by A15;
then  k <= sup (compactbelow x) by A4, LATTICE3:def_9;
then  sup (compactbelow x) in uparrow k by WAYBEL_0:18;
then  ( sup (compactbelow x) <= sup (compactbelow x) & not sup (compactbelow x) in downarrow (sup (compactbelow x)) ) by A12, A13, XBOOLE_0:def_5;
hence  contradiction by WAYBEL_0:17; ::_thesis: verum
end;
hence  x = "\/" ((compactbelow x),L) ; ::_thesis: verum
end;