:: deftheorem Def4 defines TopAugmentation YELLOW_9:def 4 :
for R being RelStr
for b₂ being TopRelStr holds
( b₂ is TopAugmentation of R iff RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of R, the InternalRel of R #) );