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: RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of S,the InternalRel of S #) by A1, YELLOW_9:def 4;
the topology of S = sigma S by WAYBEL14:23
.= sigma T by A1, YELLOW_9:52
.= the topology of A by YELLOW_9:51 ;
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