let R1, R2 be complete LATTICE; :: thesis: ( RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) implies Scott-Convergence R1 = Scott-Convergence R2 )
assume A1: RelStr(# the carrier of R1,the InternalRel of R1 #) = RelStr(# the carrier of R2,the InternalRel of R2 #) ; :: thesis: Scott-Convergence R1 = Scott-Convergence R2
then A2: Scott-Convergence R1 c= Scott-Convergence R2 by Lm19;
Scott-Convergence R2 c= Scott-Convergence R1 by A1, Lm19;
hence Scott-Convergence R1 = Scott-Convergence R2 by A2, XBOOLE_0:def 10; :: thesis: verum