let N be complete meet-continuous Lawson 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:

proof

let x be Point of N; :: according to WAYBEL30:def 4 :: thesis:

A3: now

let W be Subset of N; :: thesis:
assume that
A4: W is open and
A5: x in W ; :: 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;
reconsider y = x as Point of S by A1;
consider By being Basis of y such that
A6: 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 A4, YELLOW_8:18;
then consider K being set such that
A7: ( x in K & K in { G where G is Subset of N : ( G in BL & G c= W ) } ) by A5, TARSKI:def 4;
consider G being Subset of N such that
A8: K = G and
A9: G in BL and
A10: G c= W by A7;
consider V, F being Subset of N such that
A11: G = V \ (uparrow F) and
A12: V in sigma N and
A13: F is finite by A9;
reconsider V = V as Subset of S by A1;
A14: sigma N = sigma S by A1, YELLOW_9:52;
then A15: V is open by A12, WAYBEL14:24;
reconsider F = F as finite Subset of N by A13;
y in V by A7, A8, A11, XBOOLE_0:def 5;
then consider U1 being Subset of S such that
A16: U1 in By and
A17: U1 c= V by A15, YELLOW_8:22;
reconsider U2 = U1 as Subset of N by A1;
U1 is Filter of S by A6, A16;
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:
A18: y in U1 by A16, YELLOW_8:21;
not x in uparrow F by A7, A8, A11, XBOOLE_0:def 5;
hence x in IT by A18, XBOOLE_0:def 5; :: thesis:
U1 is open by A16, YELLOW_8:21;
then U1 in sigma S by WAYBEL14:24;
then A19: IT in BL by A14;
BL c= the topology of N by CANTOR_1:def 2;
hence IT is open by A19, PRE_TOPC:def 5; :: thesis:
IT c= G by A11, A17, XBOOLE_1:33;
hence IT c= W by A10, XBOOLE_1:1; :: thesis:

end;

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
A20: 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 ;
SF is Basis of x

proof

thus SF c= the topology of N :: according to YELLOW_8:def 2 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: a in SF ; :: thesis:
then reconsider W = a as Subset of N ;
consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that
A22: W1 = W and
( U1 \ (uparrow F) = W & x in W ) and
A23: W1 is open by A20, A21;
thus a in the topology of N by A22, A23, PRE_TOPC:def 5; :: thesis:

end;

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 ;
consider U1 being Filter of N, F being finite Subset of N, W1 being Subset of N such that
A25: ( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A20, A24;
thus x in a by A25; :: thesis:

end;

hence x in Intersect SF by SETFAM_1:58; :: thesis:
let W be Subset of N; :: thesis:
assume ( W is open & x in W ) ; :: thesis:
then consider U2 being Filter of N, F being finite Subset of N, IT being Subset of N such that
A26: ( IT = U2 \ (uparrow F) & x in IT & IT is open & IT c= W ) by A3;
take IT ; :: thesis:
thus ( IT in SF & IT c= W ) by A20, A26; :: 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
A27: ( W1 = W & U1 \ (uparrow F) = W & x in W & W1 is open ) by A20;
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 A28: ( a in the carrier of (subrelstr W) & b in the carrier of (subrelstr W) & ex_inf_of {a,b},N ) ; :: thesis:
A29: the carrier of (subrelstr W) = W by YELLOW_0:def 15;
then A30: ( a in U1 & b in U1 & not a in uparrow F & not b in uparrow F ) by A27, A28, XBOOLE_0:def 5;
then consider z being Element of N such that
A31: ( z in U1 & z <= a & z <= b ) by WAYBEL_0:def 2;
z "/\" z <= a "/\" b by A31, YELLOW_3:2;
then z <= a "/\" b by YELLOW_0:25;
then A32: a "/\" b in U1 by A31, WAYBEL_0:def 20;
for y being Element of N st y <= a "/\" b holds
not y in F

proof

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

end;

then not a "/\" b in uparrow F by WAYBEL_0:def 16;
then a "/\" b in W by A27, A32, XBOOLE_0:def 5;
hence "/\" {a,b},N in the carrier of (subrelstr W) by A29, YELLOW_0:40; :: thesis:

end;

assume A34: 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
A35: for A being Subset of N st A in J holds
subrelstr A is meet-inheriting by A34, Def4;
reconsider J' = { (uparrow A) where A is Subset of N : A in J } as Basis of x by Th16;
take J' ; :: thesis:
let W be Subset of S; :: thesis:
assume W in J' ; :: thesis:
then consider V being Subset of N such that
A36: W = uparrow V and
A37: V in J ;
A38: x in V by A37, YELLOW_8:21;
subrelstr V is meet-inheriting by A35, A37;
then V is filtered by YELLOW12:26;
then uparrow V is filtered ;
hence W is Filter of S by A1, A36, A38, WAYBEL_0:4, WAYBEL_0:25; :: thesis: