let T be complete Lawson TopLattice; :: thesis:
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 & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:51, YELLOW_9:def 4;
then reconsider B1 = sigma T as Basis of S by CANTOR_1:2;
consider R being correct lower TopAugmentation of T;
A2: RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
reconsider B2 = { ((uparrow F) ` ) where F is Subset of R : F is finite } as Basis of R by Th7;
T is TopAugmentation of T by YELLOW_9:44;
then T is Refinement of S,R by Th29;
then A3: (B1 \/ B2) \/ (INTERSECTION B1,B2) is Basis of T by YELLOW_9:59;
A4: INTERSECTION B1,B2 = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis:

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

end;

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

end;

A9: B1 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

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

end;

B2 c= { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) }

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

end;

then A12: 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;
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 A9, XBOOLE_1:12;
hence { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } is Basis of T by A3, A4, A12, XBOOLE_1:4; :: thesis: