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