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