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