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

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