let L be TopLattice; :: thesis: ( L is trivial implies L is lim-inf )
assume L is trivial ; :: thesis: L is lim-inf
then reconsider L9 = L as trivial TopLattice ;
the carrier of (ConvergenceSpace (lim_inf-Convergence L)) = the carrier of L9 by YELLOW_6:def 27;
then reconsider S = ConvergenceSpace (lim_inf-Convergence L) as non empty trivial TopSpace ;
consider x being Point of L9;
reconsider y = x as Point of S by YELLOW_6:def 27;
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