let N be complete meet-continuous Lawson 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
A2: RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of S,the InternalRel of S #) by YELLOW_9:def 4;
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 } ;
{ (uparrow A) where A is Subset of N : A in J } is Subset-Family of S

proof

{ (uparrow A) where A is Subset of N : A in J } c= bool the carrier of S

proof

let k be set ; :: 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 consider A being Subset of N such that
A3: k = uparrow A and
A in J ;
thus k in bool the carrier of S by A2, A3; :: thesis: verum

end;

hence { (uparrow A) where A is Subset of N : A in J } is Subset-Family of S ; :: 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

thus K c= the topology of S :: according to YELLOW_8:def 2 :: thesis: ( x in Intersect K & ( 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₁ ) ) ) )

proof

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

end;

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 ;
y in Intersect J by YELLOW_8:def 2;
then A8: y in A by A7, SETFAM_1:58;
A c= uparrow A by WAYBEL_0:16;
hence x in k by A1, A6, A8; :: thesis: verum

end;

hence x in Intersect K by SETFAM_1:58; :: 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 A9: ( sA is open & x in sA ) ; :: thesis: ex b₁ being Element of bool the carrier of S st
( b₁ in K & b₁ c= sA )
reconsider lA = sA as Subset of N by A2;
sigma N c= lambda N by Th10;
then A10: sigma S c= lambda N by A2, YELLOW_9:52;
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 uparrow lA in sigma S by Th14;
then A11: uparrow lA is open by A10, Th12;
lA c= uparrow lA by WAYBEL_0:16;
then consider lV1 being Subset of N such that
A12: lV1 in J and
A13: lV1 c= uparrow lA by A1, A9, A11, YELLOW_8:def 2;
reconsider sUV = uparrow lV1 as Subset of S by A2;
take sUV ; :: thesis: ( sUV in K & sUV c= sA )
thus sUV in K by A12; :: thesis: sUV c= sA
A14: sA = uparrow sA

proof

thus sA c= uparrow sA by WAYBEL_0:16; :: according to XBOOLE_0:def 10 :: thesis: uparrow sA c= sA
sA is upper by A9, WAYBEL11:def 4;
hence uparrow sA c= sA by WAYBEL_0:24; :: thesis: verum

end;

A15: uparrow sA = uparrow lA by A2, WAYBEL_0:13;
lV1 is_coarser_than uparrow lA by A13, WAYBEL12:20;
hence sUV c= sA by A14, A15, YELLOW12:28; :: thesis: verum

end;

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