let T be non empty TopSpace-like reflexive TopRelStr ; :: thesis: ( T is trivial implies T is upper )
assume A1: T is trivial ; :: 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 set ; :: 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 ;
A2: { ((downarrow x) ` ) where x is Element of T : verum } c= the topology of T

proof

let a be set ; :: 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 )
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
A3: a = (downarrow x) ` ;
a c= {}

proof

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

end;

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

end;

reconsider F = {the carrier of T} as Basis of T by A1, 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 set ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((downarrow x) ` ) where x is Element of T : verum } or a in {{} } )
assume a in { ((downarrow x) ` ) where x is Element of T : verum } ; :: thesis: a in {{} }
then consider x being Element of T such that
A8: a = (downarrow x) ` ;
A9: x <= x ;
A10: the carrier of T = {x} by A1, YELLOW_9:9;
x in downarrow x by A9, WAYBEL_0:17;
then ( a = {} or ( a = the carrier of T & not x in a ) ) by A8, A10, XBOOLE_0:def 5, ZFMISC_1:39;
hence a in {{} } by TARSKI:def 1; :: thesis: verum

end;

consider x being Element of T;
A11: x <= x ;
A12: the carrier of T = {x} by A1, YELLOW_9:9;
x in downarrow x by A11, WAYBEL_0:17;
then ( (downarrow x) ` = {} or ( (downarrow x) ` = the carrier of T & not x in (downarrow x) ` ) ) by A12, XBOOLE_0:def 5, ZFMISC_1:39;
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:37; :: thesis: verum

end;

then FinMeetCl C = {{} ,the carrier of T} by YELLOW_9:11;
then F c= FinMeetCl C by ZFMISC_1:12;
hence { ((downarrow x) ` ) where x is Element of T : verum } is prebasis of T by A2, CANTOR_1:def 5, TOPS_2:78; :: according to WAYBEL32:def 1 :: thesis: verum