let A be Subset of R^1; :: thesis: ( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
reconsider A1 = A as Subset of RealSpace by TOPMETR:12;
thus ( A is open implies for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) :: thesis: ( ( for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ) implies A is open )

proof

reconsider A1 = A as Subset of R^1 ;
A1: the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;
assume A is open ; :: thesis: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then A2: A1 in the topology of R^1 by PRE_TOPC:def 2;
let x be Real; :: thesis: ( x in A implies ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
reconsider x1 = x as Element of REAL by XREAL_0:def 1;
reconsider x1 = x1 as Element of RealSpace by METRIC_1:def 13;
assume x in A ; :: thesis: ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A )
then consider r being Real such that
A3: r > 0 and
A4: Ball (x1,r) c= A1 by A2, A1, PCOMPS_1:def 4;
].(x - r),(x + r).[ c= A1 by A4, Th7;
hence ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) by A3; :: thesis: verum

end;

assume A5: for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) ; :: thesis: A is open
for x being Element of RealSpace st x in A1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= A1 )

proof

let x be Element of RealSpace; :: thesis: ( x in A1 implies ex r being Real st
( r > 0 & Ball (x,r) c= A1 ) )
reconsider x1 = x as Real ;
assume x in A1 ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= A1 )
then consider r being Real such that
A6: r > 0 and
A7: ].(x1 - r),(x1 + r).[ c= A1 by A5;
Ball (x,r) c= A1 by A7, Th7;
hence ex r being Real st
( r > 0 & Ball (x,r) c= A1 ) by A6; :: thesis: verum

end;

then A8: A1 in Family_open_set RealSpace by PCOMPS_1:def 4;
the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;
hence A is open by A8, PRE_TOPC:def 2; :: thesis: verum