theorem Th16: :: WAYBEL25:16

for L being complete LATTICE
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 #)