let T be complete Lawson TopLattice; :: thesis: (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T
set R = the correct lower TopAugmentation of T;
reconsider K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } as prebasis of the correct lower TopAugmentation of T by Def1;
set O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ;
{ (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } c= bool the carrier of T
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } or a in bool the carrier of T )
assume a in { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } ; :: thesis: a in bool the carrier of T
then ex W being Subset of T ex x being Element of T st
( a = W \ (uparrow x) & W in sigma T ) ;
hence a in bool the carrier of T ; :: thesis: verum
end;
then reconsider O = { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } as Subset-Family of T ;
reconsider O = O as Subset-Family of T ;
set S = the Scott TopAugmentation of T;
A1: 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;
(sigma T) \/ (omega T) is prebasis of T by Def3;
then A2: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64;
omega T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A3: omega T c= the topology of T by A2;
sigma T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A4: sigma T c= the topology of T by A2;
A5: omega T = the topology of the correct lower TopAugmentation of T by Def2;
O c= the topology of T
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in O or a in the topology of T )
assume a in O ; :: thesis: a in the topology of T
then consider W being Subset of T, x being Element of T such that
A6: a = W \ (uparrow x) and
A7: W in sigma T ;
A8: a = W /\ ((uparrow x) `) by A6, SUBSET_1:13;
reconsider y = x as Element of the correct lower TopAugmentation of T by A1;
uparrow x = uparrow y by A1, WAYBEL_0:13;
then A9: (uparrow x) ` in K by A1;
K c= omega T by A5, TOPS_2:64;
then (uparrow x) ` in omega T by A9;
hence a in the topology of T by A4, A3, A7, A8, PRE_TOPC:def 1; :: thesis: verum
end;
then A10: (sigma T) \/ O c= the topology of T by A4, XBOOLE_1:8;
A11: 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;
A12: sigma T = the topology of the Scott TopAugmentation of T by YELLOW_9:51;
then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2;
then A13: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27;
A14: the carrier of the Scott TopAugmentation of T in sigma T by A12, PRE_TOPC:def 1;
K c= O
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in K or a in O )
assume a in K ; :: thesis: a in O
then consider x being Element of the correct lower TopAugmentation of T such that
A15: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
a = ([#] T) \ (uparrow y) by A1, A15, WAYBEL_0:13;
hence a in O by A11, A14; :: thesis: verum
end;
then A16: (sigma T) \/ K c= (sigma T) \/ O by XBOOLE_1:9;
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;
hence (sigma T) \/ { (W \ (uparrow x)) where W is Subset of T, x is Element of T : W in sigma T } is prebasis of T by A13, A1, A11, Th23, A16, A10, Th22; :: thesis: verum