let S be TopRelStr ; :: thesis: for T being TopAugmentation of S holds S is TopAugmentation of T
let T be TopAugmentation of S; :: thesis: S is TopAugmentation of T
thus RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by Def4; :: according to YELLOW_9:def 4 :: thesis: verum