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 #) by YELLOW_9:def 4;
T is TopAugmentation of T by YELLOW_9:44;
then A2: T is Refinement of S,R by Th29;
set K = { ((uparrow x) `) where x is Element of R : verum } ;
set O = { ((uparrow x) `) where x is Element of T : verum } ;
the topology of S = sigma T by YELLOW_9:51;
then sigma T is Basis of S by CANTOR_1:2;
then A3: sigma T is prebasis of S by YELLOW_9:27;
A4: RelStr(# the carrier of R, the InternalRel of R #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
{ ((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
A5: a = (uparrow x) ` ;
reconsider y = x as Element of R by A4;
uparrow x = uparrow y by A4, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of R : verum } by A4, A5; :: 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
A6: a = (uparrow x) ` ;
reconsider y = x as Element of T by A4;
uparrow x = uparrow y by A4, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of T : verum } by A4, A6; :: thesis: verum

end;

then reconsider O = { ((uparrow x) `) where x is Element of T : verum } as prebasis of R by Def1;
O = O ;
hence (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A3, A2, A1, A4, Th23; :: thesis: verum