let L be non empty TopRelStr ; :: thesis: ( L is lim-inf implies L is TopSpace-like )

set T = ConvergenceSpace (lim_inf-Convergence L);

assume L is lim-inf ; :: thesis: L is TopSpace-like

then A1: the topology of L = xi L

.= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def 4 ;

A2: for a being Subset-Family of L st a c= the topology of L holds

union a in the topology of L

then A3: the carrier of L in the topology of L by A1, PRE_TOPC:def 1;

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 A1, PRE_TOPC:def 1;

hence L is TopSpace-like by A3, A2; :: thesis: verum

set T = ConvergenceSpace (lim_inf-Convergence L);

assume L is lim-inf ; :: thesis: L is TopSpace-like

then A1: the topology of L = xi L

.= the topology of (ConvergenceSpace (lim_inf-Convergence L)) by WAYBEL28:def 4 ;

A2: for a being Subset-Family of L st a c= the topology of L holds

union a in the topology of L

proof

the carrier of L = the carrier of (ConvergenceSpace (lim_inf-Convergence L))
by YELLOW_6:def 24;
let a be Subset-Family of L; :: thesis: ( a c= the topology of L implies union a in the topology of L )

reconsider b = a as Subset-Family of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def 24;

assume a c= the topology of L ; :: thesis: union a in the topology of L

then union b in the topology of (ConvergenceSpace (lim_inf-Convergence L)) by A1, PRE_TOPC:def 1;

hence union a in the topology of L by A1; :: thesis: verum

end;reconsider b = a as Subset-Family of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def 24;

assume a c= the topology of L ; :: thesis: union a in the topology of L

then union b in the topology of (ConvergenceSpace (lim_inf-Convergence L)) by A1, PRE_TOPC:def 1;

hence union a in the topology of L by A1; :: thesis: verum

then A3: the carrier of L in the topology of L by A1, PRE_TOPC:def 1;

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 A1, PRE_TOPC:def 1;

hence L is TopSpace-like by A3, A2; :: thesis: verum