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 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 R being correct lower TopAugmentation of T;
reconsider K = { ((uparrow x) ` ) where x is Element of R : verum } as prebasis of R by Def1;
A1: omega T = the topology of R by Def2;
consider S being Scott TopAugmentation of T;
A2: ( RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
A3: sigma T = the topology of S by YELLOW_9:51;
then A4: ( the carrier of S in sigma T & the carrier of T = [#] T ) by 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
A5: a = (uparrow x) ` ;
reconsider y = x as Element of T by A2;
a = ([#] T) \ (uparrow y) by A2, A5, WAYBEL_0:13;
hence a in O by A2, A4; :: thesis: verum

end;

then A6: (sigma T) \/ K c= (sigma T) \/ O by XBOOLE_1:9;
(sigma T) \/ (omega T) is prebasis of T by Def3;
then ( sigma T c= (sigma T) \/ (omega T) & omega T c= (sigma T) \/ (omega T) & (sigma T) \/ (omega T) c= the topology of T ) by CANTOR_1:def 5, XBOOLE_1:7;
then A7: ( sigma T c= the topology of T & omega T c= the topology of T ) by XBOOLE_1:1;
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
A8: ( a = W \ (uparrow x) & W in sigma T ) ;
A9: a = W /\ ((uparrow x) ` ) by A8, SUBSET_1:32;
reconsider y = x as Element of R by A2;
uparrow x = uparrow y by A2, WAYBEL_0:13;
then ( (uparrow x) ` in K & K c= omega T ) by A1, A2, CANTOR_1:def 5;
then (uparrow x) ` in omega T ;
hence a in the topology of T by A7, A8, A9, PRE_TOPC:def 1; :: thesis: verum

end;

then A10: (sigma T) \/ O c= the topology of T by A7, XBOOLE_1:8;
( T is TopAugmentation of T & sigma T is Basis of S ) by A3, CANTOR_1:2, YELLOW_9:44;
then ( T is Refinement of S,R & sigma T is prebasis of S ) by Th29, YELLOW_9:27;
then (sigma T) \/ K is prebasis of T by A2, Th23;
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 A6, A10, Th22; :: thesis: verum