let L1 be lower-bounded continuous sup-Semilattice; for T being correct Lawson TopAugmentation of L1
for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let T be correct Lawson TopAugmentation of L1; for B1 being with_bottom CLbasis of L1 holds { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
let B1 be with_bottom CLbasis of L1; { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
A1:
RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of T, the InternalRel of T #)
by YELLOW_9:def 4;
{ (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } c= bool the carrier of T
then reconsider WU = { (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } as Subset-Family of T ;
reconsider WU = WU as Subset-Family of T ;
A2:
now for A being Subset of T st A is open holds
for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )reconsider BL =
{ (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } as
Basis of
T by WAYBEL19:32;
set S = the
Scott TopAugmentation of
T;
let A be
Subset of
T;
( A is open implies for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )assume A3:
A is
open
;
for pT being Point of T st pT in A holds
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )let pT be
Point of
T;
( pT in A implies ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A ) )assume
pT in A
;
ex cT being Subset of T st
( cT in WU & pT in cT & cT c= A )then consider a being
Subset of
T such that A4:
a in BL
and A5:
pT in a
and A6:
a c= A
by A3, YELLOW_9:31;
consider W,
FT being
Subset of
T such that A7:
a = W \ (uparrow FT)
and A8:
W in sigma T
and A9:
FT is
finite
by A4;
A10:
RelStr(# the
carrier of the
Scott TopAugmentation of
T, the
InternalRel of the
Scott TopAugmentation of
T #)
= RelStr(# the
carrier of
T, the
InternalRel of
T #)
by YELLOW_9:def 4;
then reconsider pS =
pT as
Element of the
Scott TopAugmentation of
T ;
reconsider W1 =
W as
Subset of the
Scott TopAugmentation of
T by A10;
sigma the
Scott TopAugmentation of
T = sigma T
by A10, YELLOW_9:52;
then A11:
W = union { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 }
by A8, WAYBEL14:33;
reconsider pL =
pS as
Element of
L1 by A1;
defpred S1[
object ,
object ]
means ex
b1,
y1 being
Element of
L1 st
(
y1 = $1 &
b1 = $2 &
b1 in B1 & not
b1 <= pL &
b1 << y1 );
A12:
Bottom L1 in B1
by WAYBEL23:def 8;
pT in W
by A5, A7, XBOOLE_0:def 5;
then consider k being
set such that A13:
pT in k
and A14:
k in { (wayabove x) where x is Element of the Scott TopAugmentation of T : x in W1 }
by A11, TARSKI:def 4;
consider xS being
Element of the
Scott TopAugmentation of
T such that A15:
k = wayabove xS
and A16:
xS in W1
by A14;
reconsider xL =
xS as
Element of
L1 by A1, A10;
xS << pS
by A13, A15, WAYBEL_3:8;
then
xL << pL
by A1, A10, WAYBEL_8:8;
then consider bL being
Element of
L1 such that A17:
bL in B1
and A18:
xL <= bL
and A19:
bL << pL
by A12, WAYBEL23:47;
reconsider FL =
FT as
Subset of
L1 by A1;
A20:
uparrow FT = uparrow FL
by A1, WAYBEL_0:13;
A21:
not
pT in uparrow FT
by A5, A7, XBOOLE_0:def 5;
A22:
for
y being
object st
y in FL holds
ex
b being
object st
S1[
y,
b]
proof
let y be
object ;
( y in FL implies ex b being object st S1[y,b] )
assume A23:
y in FL
;
ex b being object st S1[y,b]
then reconsider y1 =
y as
Element of
L1 ;
not
y1 <= pL
by A21, A20, A23, WAYBEL_0:def 16;
then consider b1 being
Element of
L1 such that A24:
(
b1 in B1 & not
b1 <= pL &
b1 << y1 )
by WAYBEL23:46;
reconsider b =
b1 as
set ;
take
b
;
S1[y,b]
take
b1
;
ex y1 being Element of L1 st
( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 )
take
y1
;
( y1 = y & b1 = b & b1 in B1 & not b1 <= pL & b1 << y1 )
thus
(
y1 = y &
b1 = b &
b1 in B1 & not
b1 <= pL &
b1 << y1 )
by A24;
verum
end; consider f being
Function such that A25:
dom f = FL
and A26:
for
y being
object st
y in FL holds
S1[
y,
f . y]
from CLASSES1:sch 1(A22);
rng f c= the
carrier of
L1
then reconsider FFL =
rng f as
Subset of
L1 ;
A29:
FFL c= B1
A32:
uparrow FL c= uparrow FFL
proof
let z be
object ;
TARSKI:def 3 ( not z in uparrow FL or z in uparrow FFL )
assume A33:
z in uparrow FL
;
z in uparrow FFL
then reconsider z1 =
z as
Element of
L1 ;
consider v1 being
Element of
L1 such that A34:
v1 <= z1
and A35:
v1 in FL
by A33, WAYBEL_0:def 16;
consider b1,
y1 being
Element of
L1 such that A36:
y1 = v1
and A37:
b1 = f . v1
and
b1 in B1
and
not
b1 <= pL
and A38:
b1 << y1
by A26, A35;
b1 << z1
by A34, A36, A38, WAYBEL_3:2;
then A39:
b1 <= z1
by WAYBEL_3:1;
b1 in FFL
by A25, A35, A37, FUNCT_1:def 3;
hence
z in uparrow FFL
by A39, WAYBEL_0:def 16;
verum
end; reconsider cT =
(wayabove bL) \ (uparrow FFL) as
Subset of
T by A1;
take cT =
cT;
( cT in WU & pT in cT & cT c= A )
(
cT = Way_Up (
bL,
FFL) &
FFL is
finite )
by A9, A25, FINSET_1:8;
hence
cT in WU
by A17, A29;
( pT in cT & cT c= A )
wayabove bL c= wayabove xL
by A18, WAYBEL_3:12;
then A40:
(wayabove bL) \ (uparrow FFL) c= (wayabove xL) \ (uparrow FL)
by A32, XBOOLE_1:35;
for
z being
Element of
L1 holds
( not
z in FFL or not
z <= pL )
then
for
z being
Element of
L1 holds
( not
z <= pL or not
z in FFL )
;
then A43:
not
pL in uparrow FFL
by WAYBEL_0:def 16;
pL in wayabove bL
by A19, WAYBEL_3:8;
hence
pT in cT
by A43, XBOOLE_0:def 5;
cT c= A
wayabove xL c= W
then
(wayabove xL) \ (uparrow FL) c= a
by A7, A20, XBOOLE_1:33;
then
(wayabove bL) \ (uparrow FFL) c= a
by A40;
hence
cT c= A
by A6;
verum end;
WU c= the topology of T
hence
{ (Way_Up (a,A)) where a is Element of L1, A is finite Subset of L1 : ( a in B1 & A c= B1 ) } is Basis of T
by A2, YELLOW_9:32; verum