let x be Element of TarskiSpace; :: thesis: x is real
MetrStruct(# the carrier of RealSpace, the distance of RealSpace #) = MetrStruct(# the carrier of TarskiSpace, the distance of TarskiSpace #) by TADef;
hence x is real ; :: thesis: verum