let T be complete Lawson TopLattice; :: thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T
consider R being correct lower TopAugmentation of T;
reconsider B2 = { ((uparrow F) ` ) where F is Subset of R : F is finite } as Basis of R by Th7;
set Z = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ;
consider S being Scott TopAugmentation of T;
A1: the topology of S = sigma T by YELLOW_9:51;
then reconsider B1 = sigma T as Basis of S by CANTOR_1:2;
A2: RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
B1 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

proof

set F9 = {} R;
reconsider G = {} R as Subset of T by A2;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B1 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume A3: x in B1 ; :: thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then reconsider x9 = x as Subset of T ;
uparrow G = uparrow ({} R) ;
then x9 \ (uparrow G) = x9 ;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A3; :: thesis: verum

end;

then A4: B1 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12;
A5: INTERSECTION B1,B2 = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } c= INTERSECTION B1,B2

let x be set ; :: thesis: ( x in INTERSECTION B1,B2 implies x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume x in INTERSECTION B1,B2 ; :: thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then consider y, z being set such that
A6: y in B1 and
A7: z in B2 and
A8: x = y /\ z by SETFAM_1:def 5;
reconsider y = y as Subset of T by A6;
A9: ([#] T) /\ y = y by XBOOLE_1:28;
consider F being Subset of R such that
A10: z = (uparrow F) ` and
A11: F is finite by A7;
reconsider G = F as Subset of T by A2;
z = (uparrow G) ` by A2, A10, WAYBEL_0:13;
then x = y \ (uparrow G) by A9, A8, XBOOLE_1:49;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A6, A11; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } or x in INTERSECTION B1,B2 )
assume x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ; :: thesis: x in INTERSECTION B1,B2
then consider W, F being Subset of T such that
A12: x = W \ (uparrow F) and
A13: W in sigma T and
A14: F is finite ;
W /\ ([#] T) = W by XBOOLE_1:28;
then A15: x = W /\ (([#] T) \ (uparrow F)) by A12, XBOOLE_1:49;
reconsider G = F as Subset of R by A2;
A16: (uparrow G) ` in B2 by A14;
(uparrow F) ` = (uparrow G) ` by A2, WAYBEL_0:13;
hence x in INTERSECTION B1,B2 by A16, A13, A15, SETFAM_1:def 5; :: thesis: verum

end;

A17: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
B2 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B2 or x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } )
assume x in B2 ; :: thesis: x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }
then consider F being Subset of R such that
A18: x = (uparrow F) ` and
A19: F is finite ;
A20: the carrier of S in B1 by A1, PRE_TOPC:def 1;
reconsider G = F as Subset of T by A2;
uparrow F = uparrow G by A2, WAYBEL_0:13;
hence x in { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by A17, A20, A2, A18, A19; :: thesis: verum

end;

then A21: B2 \/ { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } by XBOOLE_1:12;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of S,R by Th29;
then (B1 \/ B2) \/ (INTERSECTION B1,B2) is Basis of T by YELLOW_9:59;
hence { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T by A4, A5, A21, XBOOLE_1:4; :: thesis: verum