let L be complete LATTICE; :: thesis: for S being Scott TopAugmentation of L holds RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #)
let S be Scott TopAugmentation of L; :: thesis: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #)
TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) = Omega S by Th15;
hence RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4; :: thesis: verum