let T be 1 -element TopSpace-like reflexive TopRelStr ; :: thesis: T is upper
set BB = { ((downarrow x) `) where x is Element of T : verum } ;
{ ((downarrow 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 { ((downarrow x) `) where x is Element of T : verum } or a in bool the carrier of T )
assume a in { ((downarrow 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 = (downarrow x) ` ;
hence a in bool the carrier of T ; :: thesis: verum

end;

then reconsider C = { ((downarrow x) `) where x is Element of T : verum } as Subset-Family of T ;
reconsider C = C as Subset-Family of T ;
A1: { ((downarrow 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 { ((downarrow x) `) where x is Element of T : verum } or a in the topology of T )
reconsider aa = a as set by TARSKI:1;
assume a in { ((downarrow x) `) where x is Element of T : verum } ; :: thesis: a in the topology of T
then consider x being Element of T such that
A2: a = (downarrow x) ` ;
aa c= {}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in aa or y in {} )
assume A3: y in aa ; :: thesis: y in {}
A4: x <= x ;
A5: y = x by A2, A3, STRUCT_0:def 10;
x in downarrow x by A4, WAYBEL_0:17;
then A6: x in (downarrow x) /\ aa by A3, A5, XBOOLE_0:def 4;
downarrow x misses aa by A2, XBOOLE_1:79;
hence y in {} by A6; :: thesis: verum

end;

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

end;

reconsider F = { the carrier of T} as Basis of T by YELLOW_9:10;
{ ((downarrow x) `) where x is Element of T : verum } = {{}}

proof

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((downarrow x) `) where x is Element of T : verum } or a in {{}} )
reconsider aa = a as set by TARSKI:1;
assume a in { ((downarrow x) `) where x is Element of T : verum } ; :: thesis: a in {{}}
then consider x being Element of T such that
A7: a = (downarrow x) ` ;
A8: x <= x ;
A9: the carrier of T = {x} by YELLOW_9:9;
x in downarrow x by A8, WAYBEL_0:17;
then ( a = {} or ( a = the carrier of T & not x in aa ) ) by A7, A9, XBOOLE_0:def 5, ZFMISC_1:33;
hence a in {{}} by TARSKI:def 1; :: thesis: verum

end;

set x = the Element of T;
A10: the Element of T <= the Element of T ;
A11: the carrier of T = { the Element of T} by YELLOW_9:9;
the Element of T in downarrow the Element of T by A10, WAYBEL_0:17;
then ( (downarrow the Element of T) ` = {} or ( (downarrow the Element of T) ` = the carrier of T & not the Element of T in (downarrow the Element of T) ` ) ) by A11, XBOOLE_0:def 5, ZFMISC_1:33;
then {} in { ((downarrow x) `) where x is Element of T : verum } ;
hence {{}} c= { ((downarrow 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 F c= FinMeetCl C by ZFMISC_1:7;
hence { ((downarrow x) `) where x is Element of T : verum } is prebasis of T by A1, CANTOR_1:def 4, TOPS_2:64; :: according to WAYBEL32:def 1 :: thesis: verum