let x be Element of gen_R^1; :: thesis: ex y being Point of (TopSpaceMetr RealSpace) st
( x = y & U_FMT x = Balls y )
ex y being Point of (TopSpaceMetr RealSpace) st
( y = x & gen_NS_R^1 . x = Balls y ) by Def20;
hence ex y being Point of (TopSpaceMetr RealSpace) st
( x = y & U_FMT x = Balls y ) by FINTOPO2:def 6; :: thesis: verum