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
proof
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;
the carrier of L = the carrier of (ConvergenceSpace (lim_inf-Convergence L)) by YELLOW_6:def 24;
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