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
set A = the correct Scott TopAugmentation of S;
RelStr(# the carrier of the correct Scott TopAugmentation of S, the InternalRel of the correct Scott TopAugmentation of S #) = RelStr(# the carrier of S, the InternalRel of S #) by Def4;
then the correct Scott TopAugmentation of S is correct Scott TopAugmentation of T by A1, Def4;
then the topology of the correct Scott TopAugmentation of S = sigma T by Th51;
hence sigma S = sigma T by Th51; :: thesis: verum