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 C1 = lim_inf-Convergence L1;
set T1 = ConvergenceSpace (lim_inf-Convergence L1);
set C2 = lim_inf-Convergence L2;
set T2 = ConvergenceSpace (lim_inf-Convergence L2);
A2: the carrier of (ConvergenceSpace (lim_inf-Convergence L2)) = the carrier of L2 by YELLOW_6:def 27;
the topology of (ConvergenceSpace (lim_inf-Convergence L1)) = the topology of (ConvergenceSpace (lim_inf-Convergence L2))

proof

thus the topology of (ConvergenceSpace (lim_inf-Convergence L1)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L2)) by A1, Lm3; :: according to XBOOLE_0:def 10 :: thesis: the topology of (ConvergenceSpace (lim_inf-Convergence L2)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L1))
thus the topology of (ConvergenceSpace (lim_inf-Convergence L2)) c= the topology of (ConvergenceSpace (lim_inf-Convergence L1)) by A1, Lm3; :: thesis: verum

end;

hence ConvergenceSpace (lim_inf-Convergence L1) = ConvergenceSpace (lim_inf-Convergence L2) by A1, A2, YELLOW_6:def 27; :: thesis: verum