let L be TopLattice; :: thesis: ( L is trivial implies L is lim-inf )
assume L is trivial ; :: thesis: L is lim-inf
then the carrier of L is 1 -element ;
then reconsider L9 = L as 1 -element TopLattice by STRUCT_0:def 19;
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) = the carrier of L9 by YELLOW_6:def 24;
then reconsider S = ConvergenceSpace (lim_inf-Convergence L) as 1 -element TopSpace by STRUCT_0:def 19;
set x = the Point of L9;
reconsider y = the Point of L9 as Point of S by YELLOW_6:def 24;
thus the topology of L = {{},{y}} by YELLOW_9:9
.= the topology of S by YELLOW_9:9
.= xi L by WAYBEL28:def 4 ; :: according to WAYBEL33:def 2 :: thesis: verum