let N be complete Lawson meet-continuous TopLattice; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( x = y implies { (uparrow A) where A is Subset of N : A in J } is Basis of x )
assume A1: x = y ; :: thesis: { (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

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in { (uparrow A) where A is Subset of N : A in J } or k in bool the carrier of S )
assume k in { (uparrow A) where A is Subset of N : A in J } ; :: thesis: k in bool the carrier of S
then ex A being Subset of N st
( k = uparrow A & A in J ) ;
hence k in bool the carrier of S by A2; :: thesis: verum

end;

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

proof

let k be Subset of S; :: according to TOPS_2:def 1 :: thesis: ( not k in K or k is open )
assume k in K ; :: thesis: k is open
then consider A being Subset of N such that
A4: k = uparrow A and
A5: A in J ;
reconsider A9 = A as Subset of S by A2;
uparrow A9 is open by A5, Th15, YELLOW_8:12;
then uparrow A9 in the topology of S ;
then uparrow A in the topology of S by A2, WAYBEL_0:13;
hence k is open by A4; :: thesis: verum

end;

K is x -quasi_basis

proof

for k being set st k in K holds
x in k

proof

let k be set ; :: thesis: ( k in K implies x in k )
assume k in K ; :: thesis: x in k
then consider A being Subset of N such that
A6: k = uparrow A and
A7: A in J ;
A8: A c= uparrow A by WAYBEL_0:16;
y in Intersect J by YELLOW_8:def 1;
then y in A by A7, SETFAM_1:43;
hence x in k by A8, A1, A6; :: thesis: verum

end;

hence x in Intersect K by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of bool the carrier of S holds
( not b₁ is open or not x in b₁ or ex b₂ being Element of bool the carrier of S st
( b₂ in K & b₂ c= b₁ ) )
let sA be Subset of S; :: thesis: ( not sA is open or not x in sA or ex b₁ being Element of bool the carrier of S st
( b₁ in K & b₁ c= sA ) )
assume that
A9: sA is open and
A10: x in sA ; :: thesis: ex b₁ being Element of bool the carrier of S st
( b₁ in K & b₁ 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 ; :: thesis: ( sUV in K & sUV c= sA )
thus sUV in K by A14; :: thesis: 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; :: thesis: verum

end;

hence K is Basis of x by A3; :: thesis: verum

end;

hence { (uparrow A) where A is Subset of N : A in J } is Basis of x ; :: thesis: verum