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
set R = the correct lower TopAugmentation of T;
reconsider B2 = { ((uparrow F) `) where F is Subset of the correct lower TopAugmentation of T : F is finite } as Basis of the correct lower TopAugmentation of T by Th7;
set Z = { (W \ (uparrow F)) where W, F is Subset of T : ( W in sigma T & F is finite ) } ;
set S = the Scott TopAugmentation of T;
A1: the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
then reconsider B1 = sigma T as Basis of the Scott TopAugmentation of T by CANTOR_1:2;
A2: RelStr(# the carrier of the correct lower TopAugmentation of T, the InternalRel of the correct lower TopAugmentation of T #) = 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 = {} the correct lower TopAugmentation of T;
reconsider G = {} the correct lower TopAugmentation of T as Subset of T by A2;
let x be object ; :: 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 ({} the correct lower TopAugmentation of T) ;
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 object ; :: 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 the correct lower TopAugmentation of T 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 object ; :: 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 the correct lower TopAugmentation of T 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 the Scott TopAugmentation of T, the InternalRel of the Scott TopAugmentation of T #) = 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 object ; :: 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 the correct lower TopAugmentation of T such that
A18: x = (uparrow F) ` and
A19: F is finite ;
A20: the carrier of the Scott TopAugmentation of T 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 the Scott TopAugmentation of T, the correct lower TopAugmentation of T 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