let x be Point of FMT_R^1; for r being Real st r > 0 holds
].(x - r),(x + r).[ is a_neighborhood of x
let r be Real; ( r > 0 implies ].(x - r),(x + r).[ is a_neighborhood of x )
assume A1:
r > 0
; ].(x - r),(x + r).[ is a_neighborhood of x
set S = ].(x - r),(x + r).[;
set BA = { ].a,b.[ where a, b is Real : a < b } ;
now ( ].(x - r),(x + r).[ in { ].a,b.[ where a, b is Real : a < b } & { ].a,b.[ where a, b is Real : a < b } c= Family_open_set FMT_R^1 )
(
x < x + r &
x - r < x )
by A1, XREAL_1:29, XREAL_1:44;
then
x - r < x + r
by XXREAL_0:2;
hence
].(x - r),(x + r).[ in { ].a,b.[ where a, b is Real : a < b }
;
{ ].a,b.[ where a, b is Real : a < b } c= Family_open_set FMT_R^1thus
{ ].a,b.[ where a, b is Real : a < b } c= Family_open_set FMT_R^1
by Th57, FINTOPO7:def 14;
verum
then
].(x - r),(x + r).[ in Family_open_set FMT_R^1
;
then
].(x - r),(x + r).[ in { O where O is open Subset of FMT_R^1 : verum }
by FINTOPO7:def 11;
then
ex O being open Subset of FMT_R^1 st ].(x - r),(x + r).[ = O
;
then
].(x - r),(x + r).[ in U_FMT x
by A1, TOPREAL6:15, FINTOPO7:def 1;
hence
].(x - r),(x + r).[ is a_neighborhood of x
by FINTOPO7:def 5; verum