let T be 1 -element TopSpace-like reflexive TopRelStr ; :: thesis: T is lower
set BB = { ((uparrow x) `) where x is Element of T : verum } ;
reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10;
{ ((uparrow x) `) where x is Element of T : verum } c= bool the carrier of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in bool the carrier of T )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in bool the carrier of T
then ex x being Element of T st a = (uparrow x) ` ;
hence a in bool the carrier of T ; :: thesis: verum

end;

then reconsider C = { ((uparrow x) `) where x is Element of T : verum } as Subset-Family of T ;
reconsider C = C as Subset-Family of T ;
{ ((uparrow x) `) where x is Element of T : verum } = {{}}

proof

set x = the Element of T;
thus { ((uparrow x) `) where x is Element of T : verum } c= {{}} :: according to XBOOLE_0:def 10 :: thesis: {{}} c= { ((uparrow x) `) where x is Element of T : verum }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in {{}} )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in {{}}
then consider x being Element of T such that
A1: a = (uparrow x) ` ;
x <= x ;
then A2: x in uparrow x by WAYBEL_0:18;
the carrier of T = {x} by YELLOW_9:9;
then ( a = {} or ( a = the carrier of T & not x in (uparrow x) ` ) ) by A2, A1, XBOOLE_0:def 5, ZFMISC_1:33;
hence a in {{}} by TARSKI:def 1, A1; :: thesis: verum

end;

the Element of T <= the Element of T ;
then A3: the Element of T in uparrow the Element of T by WAYBEL_0:18;
the carrier of T = { the Element of T} by YELLOW_9:9;
then ( (uparrow the Element of T) ` = {} or ( (uparrow the Element of T) ` = the carrier of T & not the Element of T in (uparrow the Element of T) ` ) ) by A3, XBOOLE_0:def 5, ZFMISC_1:33;
then {} in { ((uparrow x) `) where x is Element of T : verum } ;
hence {{}} c= { ((uparrow x) `) where x is Element of T : verum } by ZFMISC_1:31; :: thesis: verum

end;

then FinMeetCl C = {{}, the carrier of T} by YELLOW_9:11;
then A4: F c= FinMeetCl C by ZFMISC_1:7;
{ ((uparrow x) `) where x is Element of T : verum } c= the topology of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((uparrow x) `) where x is Element of T : verum } or a in the topology of T )
assume a in { ((uparrow x) `) where x is Element of T : verum } ; :: thesis: a in the topology of T
then consider x being Element of T such that
A5: a = (uparrow x) ` ;
(uparrow x) ` c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (uparrow x) ` or y in {} )
x <= x ;
then A6: x in uparrow x by WAYBEL_0:18;
A7: uparrow x misses (uparrow x) ` by XBOOLE_1:79;
assume A8: y in (uparrow x) ` ; :: thesis: y in {}
then y = x by STRUCT_0:def 10;
then x in (uparrow x) /\ ((uparrow x) `) by A6, A8, XBOOLE_0:def 4;
hence y in {} by A7; :: thesis: verum

end;

then a = {} by A5;
hence a in the topology of T by PRE_TOPC:1; :: thesis: verum

end;

hence { ((uparrow x) `) where x is Element of T : verum } is prebasis of T by A4, CANTOR_1:def 4, TOPS_2:64; :: according to WAYBEL19:def 1 :: thesis: verum