for x being Element of gen_R^1 ex y being Point of (TopSpaceMetr RealSpace) st
( x = y & U_FMT x = Balls y )