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;
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 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:
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 S1[ 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 \ () = \$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 S1[W] ) from 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 \ () & x in IT & IT is open & IT c= W )
reconsider BL = { (O \ ()) 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 \ () & 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 \ () & 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 ;
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 ;
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 \ () 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 ;
reconsider V = V as Subset of S by A1;
A18: y in V by ;
A19: sigma N = sigma S by ;
then V is open by ;
then consider U1 being Subset of S such that
A20: U1 in By and
A21: U1 c= V by ;
reconsider U2 = U1 as Subset of N by A1;
U1 is Filter of S by ;
then reconsider U2 = U2 as Filter of N by ;
U2 \ () is Subset of N ;
then reconsider IT = U1 \ () as Subset of N ;
take U2 = U2; :: thesis: ex F being finite Subset of N ex IT being Subset of N st
( IT = U2 \ () & x in IT & IT is open & IT c= W )

take F = F; :: thesis: ex IT being Subset of N st
( IT = U2 \ () & x in IT & IT is open & IT c= W )

take IT = IT; :: thesis: ( IT = U2 \ () & x in IT & IT is open & IT c= W )
thus IT = U2 \ () ; :: thesis: ( x in IT & IT is open & IT c= W )
y in U1 by ;
hence x in IT by ; :: thesis: ( IT is open & IT c= W )
U1 is open by ;
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 ;
hence IT c= W by A13; :: thesis: verum
end;
SF is Basis of x
proof
A22: SF is open
proof
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 \ () = W & x in W & W1 is open ) by ;
hence a is open ; :: thesis: verum
end;
SF is x -quasi_basis
proof
for a being set st a in SF holds
x in a
proof
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 \ () = W & x in W & W1 is open ) by ;
hence x in a ; :: thesis: verum
end;
hence x in Intersect SF by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b1 being Element of bool the carrier of N holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of N st
( b2 in SF & b2 c= b1 ) )

let W be Subset of N; :: thesis: ( not W is open or not x in W or ex b1 being Element of bool the carrier of N st
( b1 in SF & b1 c= W ) )

assume that
A25: W is open and
A26: x in W ; :: thesis: ex b1 being Element of bool the carrier of N st
( b1 in SF & b1 c= W )

consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that
A27: IT = U2 \ () 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;
hence SF is Basis of x by A22; :: thesis: verum
end;
then reconsider SF = SF as Basis of x ;
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:
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 \ () = 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 () or not b in the carrier of () or not ex_inf_of {a,b},N or "/\" ({a,b},N) in the carrier of () )
assume that
A32: a in the carrier of () and
A33: b in the carrier of () and
ex_inf_of {a,b},N ; :: thesis: "/\" ({a,b},N) in the carrier of ()
A34: the carrier of () = W by YELLOW_0:def 15;
then A35: b in U1 by ;
A36: not a in uparrow F by ;
for y being Element of N st y <= a "/\" b holds
not y in F
proof
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 ;
hence not y in F by ; :: thesis: verum
end;
then A38: not a "/\" b in uparrow F by WAYBEL_0:def 16;
a in U1 by ;
then consider z being Element of N such that
A39: z in U1 and
A40: z <= a and
A41: z <= b by ;
z "/\" z <= a "/\" b by ;
then z <= a "/\" b by YELLOW_0:25;
then a "/\" b in U1 by ;
then a "/\" b in W by ;
hence "/\" ({a,b},N) in the carrier of () by ; :: thesis: verum
end;
end;
end;
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

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 = { () 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 ;
then A46: V is filtered by YELLOW12:26;
x in V by ;
hence W is Filter of S by ; :: thesis: verum