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 xi L1 = xi L2 )
A1: ( xi L1 = the topology of (ConvergenceSpace (lim_inf-Convergence L1)) & xi L2 = the topology of (ConvergenceSpace (lim_inf-Convergence L2)) ) by WAYBEL28:def 4;
assume RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) ; :: thesis: xi L1 = xi L2
hence ( xi L1 c= xi L2 & xi L2 c= xi L1 ) by A1, Lm3; :: according to XBOOLE_0:def 10 :: thesis: verum