:: deftheorem TADef defines TarskiExtension GTARSKI1:def 13 :
for M being MetrStruct
for b₂ being MetrTarskiStr holds
( b₂ is TarskiExtension of M iff MetrStruct(# the carrier of b₂, the distance of b₂ #) = MetrStruct(# the carrier of M, the distance of M #) );