let L1, L2 be up-complete /\-complete Semilattice; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2)
set C2 = lim_inf-Convergence L2;
set C1 = lim_inf-Convergence L1;
set T1 = ConvergenceSpace (lim_inf-Convergence L1);
set T2 = ConvergenceSpace (lim_inf-Convergence L2);
( the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) & the topology of (ConvergenceSpace (lim_inf-Convergence L2)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L1)) ) by A1, Lm3;
then ( the carrier of (ConvergenceSpace (lim_inf-Convergence L2)) = the carrier of L2 & the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by YELLOW_6:def 24;
hence ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) by A1, YELLOW_6:def 24; :: thesis: verum