let S, T be complete LATTICE; :: thesis: ( RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) implies sigma S = sigma T )
assume A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) ; :: thesis: sigma S = sigma T
consider A being correct Scott TopAugmentation of S;
RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of S,the InternalRel of S #) by Def4;
then A is correct Scott TopAugmentation of T by A1, Def4;
then the topology of A = sigma T by Th51;
hence sigma S = sigma T by Th51; :: thesis: verum