let T be complete Lawson TopLattice; :: thesis: (sigma T) \/ { ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T
consider R being correct lower TopAugmentation of T;
consider S being Scott TopAugmentation of T;
A1: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) & RelStr(# the carrier of R,the InternalRel of R #) = RelStr(# the carrier of T,the InternalRel of T #) ) by YELLOW_9:def 4;
set O = { ((uparrow x) ` ) where x is Element of T : verum } ;
set K = { ((uparrow x) ` ) where x is Element of R : verum } ;
{ ((uparrow x) ` ) where x is Element of T : verum } = { ((uparrow x) ` ) where x is Element of R : verum }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { ((uparrow x) ` ) where x is Element of R : verum } c= { ((uparrow x) ` ) where x is Element of T : verum }

let a be set ; :: thesis: ( a in { ((uparrow x) ` ) where x is Element of T : verum } implies a in { ((uparrow x) ` ) where x is Element of R : verum } )
assume a in { ((uparrow x) ` ) where x is Element of T : verum } ; :: thesis: a in { ((uparrow x) ` ) where x is Element of R : verum }
then consider x being Element of T such that
A2: a = (uparrow x) ` ;
reconsider y = x as Element of R by A1;
uparrow x = uparrow y by A1, WAYBEL_0:13;
hence a in { ((uparrow x) ` ) where x is Element of R : verum } by A1, A2; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) ` ) where x is Element of R : verum } or a in { ((uparrow x) ` ) where x is Element of T : verum } )
assume a in { ((uparrow x) ` ) where x is Element of R : verum } ; :: thesis: a in { ((uparrow x) ` ) where x is Element of T : verum }
then consider x being Element of R such that
A3: a = (uparrow x) ` ;
reconsider y = x as Element of T by A1;
uparrow x = uparrow y by A1, WAYBEL_0:13;
hence a in { ((uparrow x) ` ) where x is Element of T : verum } by A1, A3; :: thesis: verum

end;

then reconsider O = { ((uparrow x) ` ) where x is Element of T : verum } as prebasis of R by Def1;
the topology of S = sigma T by YELLOW_9:51;
then ( sigma T is Basis of S & T is TopAugmentation of T ) by CANTOR_1:2, YELLOW_9:44;
then ( sigma T is prebasis of S & T is Refinement of S,R & O = O ) by Th29, YELLOW_9:27;
hence (sigma T) \/ { ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T by A1, Th23; :: thesis: verum