let L be complete Scott TopLattice; ( 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) }
; L is algebraic
thus
for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )
; WAYBEL_8:def 4 ( L is up-complete & L is satisfying_axiom_K )
thus
L is up-complete
; L is satisfying_axiom_K
let x be Element of L; WAYBEL_8:def 3 x = "\/" ((compactbelow x),L)
set y = sup (compactbelow x);
set cx = compactbelow x;
set dx = downarrow x;
set dy = downarrow (sup (compactbelow x));
now 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
;
contradictionthen 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;
verum
hence
x = "\/" ((compactbelow x),L)
; verum