let L1 be lower-bounded continuous sup-Semilattice; for T being Scott TopAugmentation of L1
for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
let T be Scott TopAugmentation of L1; for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
let b be Basis of T; { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
set b2 = { (wayabove (inf u)) where u is Subset of T : u in b } ;
{ (wayabove (inf u)) where u is Subset of T : u in b } c= bool the carrier of T
then reconsider b2 = { (wayabove (inf u)) where u is Subset of T : u in b } as Subset-Family of T ;
reconsider b1 = { (wayabove x) where x is Element of T : verum } as Basis of T by WAYBEL11:45;
A1:
now for A being Subset of T st A is open holds
for a being Point of T st a in A holds
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A )let A be
Subset of
T;
( A is open implies for a being Point of T st a in A holds
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A ) )assume A2:
A is
open
;
for a being Point of T st a in A holds
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A )let a be
Point of
T;
( a in A implies ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A ) )assume
a in A
;
ex u being Element of K32( the carrier of T) st
( u in b2 & a in u & u c= A )then consider C being
Subset of
T such that A3:
C in b1
and A4:
a in C
and A5:
C c= A
by A2, YELLOW_9:31;
C is
open
by A3, YELLOW_8:10;
then consider D being
Subset of
T such that A6:
D in b
and A7:
a in D
and A8:
D c= C
by A4, YELLOW_9:31;
D is
open
by A6, YELLOW_8:10;
then consider E being
Subset of
T such that A9:
E in b1
and A10:
a in E
and A11:
E c= D
by A7, YELLOW_9:31;
consider z being
Element of
T such that A12:
E = wayabove z
by A9;
take u =
wayabove (inf D);
( u in b2 & a in u & u c= A )thus
u in b2
by A6;
( a in u & u c= A )reconsider a1 =
a as
Element of
T ;
consider x being
Element of
T such that A13:
C = wayabove x
by A3;
z << a1
by A10, A12, WAYBEL_3:8;
then consider y being
Element of
T such that A14:
z << y
and A15:
y << a1
by WAYBEL_4:52;
(
inf D is_<=_than D &
y in wayabove z )
by A14, WAYBEL_3:8, YELLOW_0:33;
then
inf D <= y
by A11, A12, LATTICE3:def 8;
then
inf D << a1
by A15, WAYBEL_3:2;
hence
a in u
by WAYBEL_3:8;
u c= AA16:
wayabove x c= uparrow x
by WAYBEL_3:11;
(
ex_inf_of uparrow x,
T &
ex_inf_of D,
T )
by YELLOW_0:17;
then
inf (uparrow x) <= inf D
by A13, A8, A16, XBOOLE_1:1, YELLOW_0:35;
then
x <= inf D
by WAYBEL_0:39;
then
wayabove (inf D) c= C
by A13, WAYBEL_3:12;
hence
u c= A
by A5;
verum end;
b2 c= the topology of T
hence
{ (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T
by A1, YELLOW_9:32; verum