let N be complete Lawson meet-continuous TopLattice; :: thesis: for S being Scott TopAugmentation of N holds

( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

let S be Scott TopAugmentation of N; :: thesis: ( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

for W being Subset of S st W in J holds

W is Filter of S

let x be Point of S; :: thesis: ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S

reconsider y = x as Point of N by A1;

consider J being Basis of y such that

A43: for A being Subset of N st A in J holds

subrelstr A is meet-inheriting by A42;

reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;

take J9 ; :: thesis: for W being Subset of S st W in J9 holds

W is Filter of S

let W be Subset of S; :: thesis: ( W in J9 implies W is Filter of S )

assume W in J9 ; :: thesis: W is Filter of S

then consider V being Subset of N such that

A44: W = uparrow V and

A45: V in J ;

subrelstr V is meet-inheriting by A43, A45;

then A46: V is filtered by YELLOW12:26;

x in V by A45, YELLOW_8:12;

hence W is Filter of S by A46, A1, A44, WAYBEL_0:4, WAYBEL_0:25; :: thesis: verum

( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

let S be Scott TopAugmentation of N; :: thesis: ( ( for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ) iff N is with_open_semilattices )

A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of S, the InternalRel of S #) by YELLOW_9:def 4;

hereby :: thesis: ( N is with_open_semilattices implies for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S )

assume A42:
N is with_open_semilattices
; :: thesis: for x being Point of S ex J being Basis of x st for W being Subset of S st W in J holds

W is Filter of S )

assume A2:
for x being Point of S ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S ; :: thesis: N is with_open_semilattices

thus N is with_open_semilattices :: thesis: verum

end;for W being Subset of S st W in J holds

W is Filter of S ; :: thesis: N is with_open_semilattices

thus N is with_open_semilattices :: thesis: verum

proof

let x be Point of N; :: according to WAYBEL30:def 4 :: thesis: ex J being Basis of x st

for A being Subset of N st A in J holds

subrelstr A is meet-inheriting

defpred S_{1}[ set ] means ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st

( $1 = W1 & U1 \ (uparrow F) = $1 & x in $1 & W1 is open );

consider SF being Subset-Family of N such that

A3: for W being Subset of N holds

( W in SF iff S_{1}[W] )
from SUBSET_1:sch 3();

reconsider SF = SF as Subset-Family of N ;

take SF ; :: thesis: for A being Subset of N st A in SF holds

subrelstr A is meet-inheriting

let W be Subset of N; :: thesis: ( W in SF implies subrelstr W is meet-inheriting )

assume W in SF ; :: thesis: subrelstr W is meet-inheriting

then consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that

W1 = W and

A31: U1 \ (uparrow F) = W and

x in W and

W1 is open by A3;

set SW = subrelstr W;

thus subrelstr W is meet-inheriting :: thesis: verum

end;for A being Subset of N st A in J holds

subrelstr A is meet-inheriting

defpred S

( $1 = W1 & U1 \ (uparrow F) = $1 & x in $1 & W1 is open );

consider SF being Subset-Family of N such that

A3: for W being Subset of N holds

( W in SF iff S

reconsider SF = SF as Subset-Family of N ;

A4: now :: thesis: for W being Subset of N st W is open & x in W holds

ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

SF is Basis of x
ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

reconsider BL = { (O \ (uparrow F)) where O, F is Subset of N : ( O in sigma N & F is finite ) } as Basis of N by WAYBEL19:32;

A5: BL c= the topology of N by TOPS_2:64;

reconsider y = x as Point of S by A1;

let W be Subset of N; :: thesis: ( W is open & x in W implies ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) )

assume that

A6: W is open and

A7: x in W ; :: thesis: ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

consider By being Basis of y such that

A8: for A being Subset of S st A in By holds

A is Filter of S by A2;

W = union { G where G is Subset of N : ( G in BL & G c= W ) } by A6, YELLOW_8:9;

then consider K being set such that

A9: x in K and

A10: K in { G where G is Subset of N : ( G in BL & G c= W ) } by A7, TARSKI:def 4;

consider G being Subset of N such that

A11: K = G and

A12: G in BL and

A13: G c= W by A10;

consider V, F being Subset of N such that

A14: G = V \ (uparrow F) and

A15: V in sigma N and

A16: F is finite by A12;

reconsider F = F as finite Subset of N by A16;

A17: not x in uparrow F by A9, A11, A14, XBOOLE_0:def 5;

reconsider V = V as Subset of S by A1;

A18: y in V by A9, A11, A14, XBOOLE_0:def 5;

A19: sigma N = sigma S by A1, YELLOW_9:52;

then V is open by A15, WAYBEL14:24;

then consider U1 being Subset of S such that

A20: U1 in By and

A21: U1 c= V by A18, YELLOW_8:13;

reconsider U2 = U1 as Subset of N by A1;

U1 is Filter of S by A8, A20;

then reconsider U2 = U2 as Filter of N by A1, WAYBEL_0:4, WAYBEL_0:25;

U2 \ (uparrow F) is Subset of N ;

then reconsider IT = U1 \ (uparrow F) as Subset of N ;

take U2 = U2; :: thesis: ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

take F = F; :: thesis: ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

take IT = IT; :: thesis: ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

thus IT = U2 \ (uparrow F) ; :: thesis: ( x in IT & IT is open & IT c= W )

y in U1 by A20, YELLOW_8:12;

hence x in IT by A17, XBOOLE_0:def 5; :: thesis: ( IT is open & IT c= W )

U1 is open by A20, YELLOW_8:12;

then U1 in sigma S by WAYBEL14:24;

then IT in BL by A19;

hence IT is open by A5; :: thesis: IT c= W

IT c= G by A14, A21, XBOOLE_1:33;

hence IT c= W by A13; :: thesis: verum

end;A5: BL c= the topology of N by TOPS_2:64;

reconsider y = x as Point of S by A1;

let W be Subset of N; :: thesis: ( W is open & x in W implies ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) )

assume that

A6: W is open and

A7: x in W ; :: thesis: ex U2 being Filter of N ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

consider By being Basis of y such that

A8: for A being Subset of S st A in By holds

A is Filter of S by A2;

W = union { G where G is Subset of N : ( G in BL & G c= W ) } by A6, YELLOW_8:9;

then consider K being set such that

A9: x in K and

A10: K in { G where G is Subset of N : ( G in BL & G c= W ) } by A7, TARSKI:def 4;

consider G being Subset of N such that

A11: K = G and

A12: G in BL and

A13: G c= W by A10;

consider V, F being Subset of N such that

A14: G = V \ (uparrow F) and

A15: V in sigma N and

A16: F is finite by A12;

reconsider F = F as finite Subset of N by A16;

A17: not x in uparrow F by A9, A11, A14, XBOOLE_0:def 5;

reconsider V = V as Subset of S by A1;

A18: y in V by A9, A11, A14, XBOOLE_0:def 5;

A19: sigma N = sigma S by A1, YELLOW_9:52;

then V is open by A15, WAYBEL14:24;

then consider U1 being Subset of S such that

A20: U1 in By and

A21: U1 c= V by A18, YELLOW_8:13;

reconsider U2 = U1 as Subset of N by A1;

U1 is Filter of S by A8, A20;

then reconsider U2 = U2 as Filter of N by A1, WAYBEL_0:4, WAYBEL_0:25;

U2 \ (uparrow F) is Subset of N ;

then reconsider IT = U1 \ (uparrow F) as Subset of N ;

take U2 = U2; :: thesis: ex F being finite Subset of N ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

take F = F; :: thesis: ex IT being Subset of N st

( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

take IT = IT; :: thesis: ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W )

thus IT = U2 \ (uparrow F) ; :: thesis: ( x in IT & IT is open & IT c= W )

y in U1 by A20, YELLOW_8:12;

hence x in IT by A17, XBOOLE_0:def 5; :: thesis: ( IT is open & IT c= W )

U1 is open by A20, YELLOW_8:12;

then U1 in sigma S by WAYBEL14:24;

then IT in BL by A19;

hence IT is open by A5; :: thesis: IT c= W

IT c= G by A14, A21, XBOOLE_1:33;

hence IT c= W by A13; :: thesis: verum

proof

then reconsider SF = SF as Basis of x ;
A22:
SF is open

end;proof

SF is x -quasi_basis
let a be Subset of N; :: according to TOPS_2:def 1 :: thesis: ( not a in SF or a is open )

assume A23: a in SF ; :: thesis: a is open

reconsider W = a as Subset of N ;

ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st

( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A23;

hence a is open ; :: thesis: verum

end;assume A23: a in SF ; :: thesis: a is open

reconsider W = a as Subset of N ;

ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st

( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A23;

hence a is open ; :: thesis: verum

proof

hence
SF is Basis of x
by A22; :: thesis: verum
for a being set st a in SF holds

x in a_{1} being Element of bool the carrier of N holds

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

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

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

( b_{1} in SF & b_{1} c= W ) )

assume that

A25: W is open and

A26: x in W ; :: thesis: ex b_{1} being Element of bool the carrier of N st

( b_{1} in SF & b_{1} c= W )

consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that

A27: IT = U2 \ (uparrow F) and

A28: x in IT and

A29: IT is open and

A30: IT c= W by A25, A26, A4;

take IT ; :: thesis: ( IT in SF & IT c= W )

thus ( IT in SF & IT c= W ) by A3, A27, A28, A29, A30; :: thesis: verum

end;x in a

proof

hence
x in Intersect SF
by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b
let a be set ; :: thesis: ( a in SF implies x in a )

assume A24: a in SF ; :: thesis: x in a

then reconsider W = a as Subset of N ;

ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st

( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A24;

hence x in a ; :: thesis: verum

end;assume A24: a in SF ; :: thesis: x in a

then reconsider W = a as Subset of N ;

ex U1 being Filter of N ex F being finite Subset of N ex W1 being Subset of N st

( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A3, A24;

hence x in a ; :: thesis: verum

( not b

( b

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

( b

assume that

A25: W is open and

A26: x in W ; :: thesis: ex b

( b

consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that

A27: IT = U2 \ (uparrow F) and

A28: x in IT and

A29: IT is open and

A30: IT c= W by A25, A26, A4;

take IT ; :: thesis: ( IT in SF & IT c= W )

thus ( IT in SF & IT c= W ) by A3, A27, A28, A29, A30; :: thesis: verum

take SF ; :: thesis: for A being Subset of N st A in SF holds

subrelstr A is meet-inheriting

let W be Subset of N; :: thesis: ( W in SF implies subrelstr W is meet-inheriting )

assume W in SF ; :: thesis: subrelstr W is meet-inheriting

then consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that

W1 = W and

A31: U1 \ (uparrow F) = W and

x in W and

W1 is open by A3;

set SW = subrelstr W;

thus subrelstr W is meet-inheriting :: thesis: verum

proof

let a, b be Element of N; :: according to YELLOW_0:def 16 :: thesis: ( not a in the carrier of (subrelstr W) or not b in the carrier of (subrelstr W) or not ex_inf_of {a,b},N or "/\" ({a,b},N) in the carrier of (subrelstr W) )

assume that

A32: a in the carrier of (subrelstr W) and

A33: b in the carrier of (subrelstr W) and

ex_inf_of {a,b},N ; :: thesis: "/\" ({a,b},N) in the carrier of (subrelstr W)

A34: the carrier of (subrelstr W) = W by YELLOW_0:def 15;

then A35: b in U1 by A31, A33, XBOOLE_0:def 5;

A36: not a in uparrow F by A34, A31, A32, XBOOLE_0:def 5;

for y being Element of N st y <= a "/\" b holds

not y in F

a in U1 by A34, A31, A32, XBOOLE_0:def 5;

then consider z being Element of N such that

A39: z in U1 and

A40: z <= a and

A41: z <= b by A35, WAYBEL_0:def 2;

z "/\" z <= a "/\" b by A40, A41, YELLOW_3:2;

then z <= a "/\" b by YELLOW_0:25;

then a "/\" b in U1 by A39, WAYBEL_0:def 20;

then a "/\" b in W by A38, A31, XBOOLE_0:def 5;

hence "/\" ({a,b},N) in the carrier of (subrelstr W) by A34, YELLOW_0:40; :: thesis: verum

end;assume that

A32: a in the carrier of (subrelstr W) and

A33: b in the carrier of (subrelstr W) and

ex_inf_of {a,b},N ; :: thesis: "/\" ({a,b},N) in the carrier of (subrelstr W)

A34: the carrier of (subrelstr W) = W by YELLOW_0:def 15;

then A35: b in U1 by A31, A33, XBOOLE_0:def 5;

A36: not a in uparrow F by A34, A31, A32, XBOOLE_0:def 5;

for y being Element of N st y <= a "/\" b holds

not y in F

proof

then A38:
not a "/\" b in uparrow F
by WAYBEL_0:def 16;
A37:
a "/\" b <= a
by YELLOW_0:23;

let y be Element of N; :: thesis: ( y <= a "/\" b implies not y in F )

assume y <= a "/\" b ; :: thesis: not y in F

then y <= a by A37, ORDERS_2:3;

hence not y in F by A36, WAYBEL_0:def 16; :: thesis: verum

end;let y be Element of N; :: thesis: ( y <= a "/\" b implies not y in F )

assume y <= a "/\" b ; :: thesis: not y in F

then y <= a by A37, ORDERS_2:3;

hence not y in F by A36, WAYBEL_0:def 16; :: thesis: verum

a in U1 by A34, A31, A32, XBOOLE_0:def 5;

then consider z being Element of N such that

A39: z in U1 and

A40: z <= a and

A41: z <= b by A35, WAYBEL_0:def 2;

z "/\" z <= a "/\" b by A40, A41, YELLOW_3:2;

then z <= a "/\" b by YELLOW_0:25;

then a "/\" b in U1 by A39, WAYBEL_0:def 20;

then a "/\" b in W by A38, A31, XBOOLE_0:def 5;

hence "/\" ({a,b},N) in the carrier of (subrelstr W) by A34, YELLOW_0:40; :: thesis: verum

for W being Subset of S st W in J holds

W is Filter of S

let x be Point of S; :: thesis: ex J being Basis of x st

for W being Subset of S st W in J holds

W is Filter of S

reconsider y = x as Point of N by A1;

consider J being Basis of y such that

A43: for A being Subset of N st A in J holds

subrelstr A is meet-inheriting by A42;

reconsider J9 = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;

take J9 ; :: thesis: for W being Subset of S st W in J9 holds

W is Filter of S

let W be Subset of S; :: thesis: ( W in J9 implies W is Filter of S )

assume W in J9 ; :: thesis: W is Filter of S

then consider V being Subset of N such that

A44: W = uparrow V and

A45: V in J ;

subrelstr V is meet-inheriting by A43, A45;

then A46: V is filtered by YELLOW12:26;

x in V by A45, YELLOW_8:12;

hence W is Filter of S by A46, A1, A44, WAYBEL_0:4, WAYBEL_0:25; :: thesis: verum