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

K is Basis of x

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

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

K is Basis of x

proof

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

end;proof

K is x -quasi_basis
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;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

proof

hence
K is Basis of x
by A3; :: thesis: verum
for k being set st k in K holds

x in k_{1} being Element of bool the carrier of S holds

( not b_{1} is open or not x in b_{1} or ex b_{2} being Element of bool the carrier of S st

( b_{2} in K & b_{2} c= b_{1} ) )

let sA be Subset of S; :: thesis: ( not sA is open or not x in sA or ex b_{1} being Element of bool the carrier of S st

( b_{1} in K & b_{1} c= sA ) )

assume that

A9: sA is open and

A10: x in sA ; :: thesis: ex b_{1} being Element of bool the carrier of S st

( b_{1} in K & b_{1} 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;x in k

proof

hence
x in Intersect K
by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b
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;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

( not b

( b

let sA be Subset of S; :: thesis: ( not sA is open or not x in sA or ex b

( b

assume that

A9: sA is open and

A10: x in sA ; :: thesis: ex b

( b

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