theorem :: WAYBEL30:5

for S being complete Scott TopLattice
for T being complete LATTICE
for A being Scott TopAugmentation of T st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) holds
TopRelStr(# the carrier of A, the InternalRel of A, the topology of A #) = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #)