let S be complete Scott TopLattice; :: thesis: 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 #)
let T be complete LATTICE; :: thesis: 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 #)
let A be Scott TopAugmentation of T; :: thesis: ( RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) implies 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 #) )
assume A1: RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) ; :: thesis: 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 #)
A2: the topology of S = sigma S by WAYBEL14:23
.= sigma T by A1, YELLOW_9:52
.= the topology of A by YELLOW_9:51 ;
RelStr(# the carrier of A, the InternalRel of A #) = RelStr(# the carrier of S, the InternalRel of S #) by A1, YELLOW_9:def 4;
hence 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 #) by A2; :: thesis: verum