let N be complete Lawson meet-continuous TopLattice; for S being Scott TopAugmentation of N
for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let S be Scott TopAugmentation of N; for x being Point of S
for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let x be Point of S; for y being Point of N
for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let y be Point of N; for J being Basis of y st x = y holds
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
let J be Basis of y; ( x = y implies { (uparrow A) where A is Subset of N : A in J } is Basis of x )
assume A1:
x = y
; { (uparrow A) where A is Subset of N : A in J } is Basis of x
set Z = { (uparrow A) where A is Subset of N : A in J } ;
set K = { (uparrow A) where A is Subset of N : A in J } ;
A2:
RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #)
by YELLOW_9:def 4;
{ (uparrow A) where A is Subset of N : A in J } c= bool the carrier of S
then reconsider K = { (uparrow A) where A is Subset of N : A in J } as Subset-Family of S ;
K is Basis of x
proof
A3:
K is
open
K is
x -quasi_basis
proof
for
k being
set st
k in K holds
x in k
hence
x in Intersect K
by SETFAM_1:43;
YELLOW_8:def 1 for b1 being Element of bool the carrier of S holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of S st
( b2 in K & b2 c= b1 ) )
let sA be
Subset of
S;
( not sA is open or not x in sA or ex b1 being Element of bool the carrier of S st
( b1 in K & b1 c= sA ) )
assume that A9:
sA is
open
and A10:
x in sA
;
ex b1 being Element of bool the carrier of S st
( b1 in K & b1 c= sA )
sA is
upper
by A9, WAYBEL11:def 4;
then A11:
uparrow sA c= sA
by WAYBEL_0:24;
reconsider lA =
sA as
Subset of
N by A2;
N is
correct Lawson TopAugmentation of
S
by A2, YELLOW_9:def 4;
then
lA is
open
by A9, WAYBEL19:37;
then
lA in lambda N
by Th12;
then A12:
uparrow lA in sigma S
by Th14;
A13:
lA c= uparrow lA
by WAYBEL_0:16;
sigma N c= lambda N
by Th10;
then
sigma S c= lambda N
by A2, YELLOW_9:52;
then
uparrow lA is
open
by A12, Th12;
then consider lV1 being
Subset of
N such that A14:
lV1 in J
and A15:
lV1 c= uparrow lA
by A13, A1, A10, YELLOW_8:def 1;
reconsider sUV =
uparrow lV1 as
Subset of
S by A2;
take
sUV
;
( sUV in K & sUV c= sA )
thus
sUV in K
by A14;
sUV c= sA
A16:
lV1 is_coarser_than uparrow lA
by A15, WAYBEL12:16;
sA c= uparrow sA
by WAYBEL_0:16;
then A17:
sA = uparrow sA
by A11;
uparrow sA = uparrow lA
by A2, WAYBEL_0:13;
hence
sUV c= sA
by A16, A17, YELLOW12:28;
verum
end;
hence
K is
Basis of
x
by A3;
verum
end;
hence
{ (uparrow A) where A is Subset of N : A in J } is Basis of x
; verum