let T be complete Lawson TopLattice; { (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 ) }
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 TARSKI:def 3,
XBOOLE_0:def 10 { (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 ;
( 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)
;
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;
verum
end;
let x be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
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 ) }
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; verum