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
consider R being correct lower TopAugmentation of T;
reconsider K = { ((uparrow x) ` ) where x is Element of R : verum } as prebasis of R 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 set ; :: 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 ;
consider S being Scott TopAugmentation of T;
A1: RelStr(# the carrier of R,the InternalRel of R #) = 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:78;
omega T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A3: omega T c= the topology of T by A2, XBOOLE_1:1;
sigma T c= (sigma T) \/ (omega T) by XBOOLE_1:7;
then A4: sigma T c= the topology of T by A2, XBOOLE_1:1;
A5: omega T = the topology of R by Def2;
O c= the topology of T

proof

let a be set ; :: 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:32;
reconsider y = x as Element of R 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:78;
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 S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
A12: sigma T = the topology of S by YELLOW_9:51;
then sigma T is Basis of S by CANTOR_1:2;
then A13: sigma T is prebasis of S by YELLOW_9:27;
A14: the carrier of S in sigma T by A12, PRE_TOPC:def 1;
K c= O

proof

let a be set ; :: 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 R 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 S,R 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