let x be Point of FMT_R^1; :: thesis: for r being Real st r > 0 holds
].(x - r),(x + r).[ is a_neighborhood of x
let r be Real; :: thesis: ( r > 0 implies ].(x - r),(x + r).[ is a_neighborhood of x )
assume A1: r > 0 ; :: thesis: ].(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 :: thesis: ( ].(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 } ; :: thesis: { ].a,b.[ where a, b is Real : a < b } c= Family_open_set FMT_R^1
thus { ].a,b.[ where a, b is Real : a < b } c= Family_open_set FMT_R^1 by Th57, FINTOPO7:def 14; :: thesis: verum

end;

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; :: thesis: verum