let N be complete Lawson meet-continuous TopLattice; :: thesis:
let S be Scott TopAugmentation of N; :: thesis:
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:

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:

let x be Point of N; :: according to WAYBEL30:def 4 :: thesis:
defpred S₁[ 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₁[W] ) from SUBSET_1:sch 3();
reconsider SF = SF as Subset-Family of N ;

A4: now :: thesis:

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:
assume that
A6: W is open and
A7: x in W ; :: thesis:
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:
take F = F; :: thesis:
take IT = IT; :: thesis:
thus IT = U2 \ (uparrow F) ; :: thesis:
y in U1 by A20, YELLOW_8:12;
hence x in IT by A17, XBOOLE_0:def 5; :: thesis:
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= G by A14, A21, XBOOLE_1:33;
hence IT c= W by A13; :: thesis:

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:
assume A23: a in SF ; :: thesis:
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:

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:
assume A24: a in SF ; :: thesis:
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:

end;

hence x in Intersect SF by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis:
let W be Subset of N; :: thesis:
assume that
A25: W is open and
A26: x in W ; :: thesis:
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:
thus ( IT in SF & IT c= W ) by A3, A27, A28, A29, A30; :: thesis:

end;

hence SF is Basis of x by A22; :: thesis:

end;

then reconsider SF = SF as Basis of x ;
take SF ; :: thesis:
let W be Subset of N; :: thesis:
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 \ (uparrow F) = W and
x in W and
W1 is open by A3;
set SW = subrelstr W;
thus subrelstr W is meet-inheriting :: thesis:

proof

let a, b be Element of N; :: according to YELLOW_0:def 16 :: thesis:
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:
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

A37: a "/\" b <= a by YELLOW_0:23;
let y be Element of N; :: thesis:
assume y <= a "/\" b ; :: thesis:
then y <= a by A37, ORDERS_2:3;
hence not y in F by A36, WAYBEL_0:def 16; :: thesis:

end;

then A38: not a "/\" b in uparrow F by WAYBEL_0:def 16;
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:

end;

assume A42: N is with_open_semilattices ; :: thesis:
let x be Point of S; :: thesis:
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:
let W be Subset of S; :: thesis:
assume W in J9 ; :: thesis:
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: