let T be non empty TopSpace-like reflexive TopRelStr ; :: thesis: ( T is trivial implies T is lower )
assume A1: T is trivial ; :: thesis: T is lower
set BB = { ((uparrow x) ` ) where x is Element of T : verum } ;
{ ((uparrow 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 { ((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 ;
A2: { ((uparrow 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 { ((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
A3: a = (uparrow 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 {}
then ( y in the carrier of T & x <= x ) by A3;
then ( y = x & x in uparrow x ) by A1, STRUCT_0:def 10, WAYBEL_0:18;
then ( x in (uparrow x) /\ a & uparrow x misses a ) by A3, A4, XBOOLE_0:def 4, XBOOLE_1:79;
hence y in {} by 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;
{ ((uparrow x) ` ) where x is Element of T : verum } = {{} }

proof

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 set ; :: 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
A5: a = (uparrow x) ` ;
x <= x ;
then ( the carrier of T = {x} & x in uparrow x ) by A1, WAYBEL_0:18, YELLOW_9:9;
then ( a = {} or ( a = the carrier of T & not x in a ) ) by A5, XBOOLE_0:def 5, ZFMISC_1:39;
hence a in {{} } by TARSKI:def 1; :: thesis: verum

end;

consider x being Element of T;
x <= x ;
then ( the carrier of T = {x} & x in uparrow x ) by A1, WAYBEL_0:18, YELLOW_9:9;
then ( (uparrow x) ` = {} or ( (uparrow x) ` = the carrier of T & not x in (uparrow x) ` ) ) by XBOOLE_0:def 5, ZFMISC_1:39;
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: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 { ((uparrow x) ` ) where x is Element of T : verum } is prebasis of T by A2, CANTOR_1:def 5; :: according to WAYBEL19:def 1 :: thesis: verum