let L be non empty TopRelStr ; :: thesis: ( L is lim-inf implies L is TopSpace-like )
assume A1: L is lim-inf ; :: thesis: L is TopSpace-like
set T = ConvergenceSpace (lim_inf-Convergence L);
A2: the topology of L = xi L by A1, Def2
.= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def 4 ;
the carrier of L = the carrier of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def 27;
then A3: the carrier of L in the topology of L by A2, PRE_TOPC:def 1;
A4: for a being Subset-Family of L st a c= the topology of L holds
union a in the topology of L

proof

let a be Subset-Family of L; :: thesis: ( a c= the topology of L implies union a in the topology of L )
assume A5: a c= the topology of L ; :: thesis: union a in the topology of L
reconsider b = a as Subset-Family of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def 27;
union b in the topology of (ConvergenceSpace (lim_inf-Convergence L)) by A2, A5, PRE_TOPC:def 1;
hence union a in the topology of L by A2; :: thesis: verum

end;

for a, b being Subset of L st a in the topology of L & b in the topology of L holds
a /\ b in the topology of L by A2, PRE_TOPC:def 1;
hence L is TopSpace-like by A3, A4, PRE_TOPC:def 1; :: thesis: verum