let T be complete Lawson TopLattice; :: thesis: (sigma T) \/ { ((uparrow x) `) where x is Element of T : verum } is prebasis of T
set R = the correct lower TopAugmentation of T;
set S = the Scott TopAugmentation of T;
A1: 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;
T is TopAugmentation of T by YELLOW_9:44;
then A2: T is Refinement of the Scott TopAugmentation of T, the correct lower TopAugmentation of T by Th29;
set K = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ;
set O = { ((uparrow x) `) where x is Element of T : verum } ;
the topology of the Scott TopAugmentation of T = sigma T by YELLOW_9:51;
then sigma T is Basis of the Scott TopAugmentation of T by CANTOR_1:2;
then A3: sigma T is prebasis of the Scott TopAugmentation of T by YELLOW_9:27;
A4: 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;
{ ((uparrow x) `) where x is Element of T : verum } = { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum }

proof

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

let a be object ; :: thesis: ( a in { ((uparrow x) `) where x is Element of T : verum } implies a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum }
then consider x being Element of T such that
A5: a = (uparrow x) ` ;
reconsider y = x as Element of the correct lower TopAugmentation of T by A4;
uparrow x = uparrow y by A4, WAYBEL_0:13;
hence a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } by A4, A5; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } or a in { ((uparrow x) `) where x is Element of T : verum } )
assume a in { ((uparrow x) `) where x is Element of the correct lower TopAugmentation of T : verum } ; :: thesis: a in { ((uparrow x) `) where x is Element of T : verum }
then consider x being Element of the correct lower TopAugmentation of T 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 the correct lower TopAugmentation of T 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