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 )

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 )

the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;

hence A is open by A8, PRE_TOPC:def 2; :: thesis: verum

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

assume A5:
for x being Real st x in A holds
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;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

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

then A8:
A1 in Family_open_set RealSpace
by PCOMPS_1:def 4;
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;( 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

the topology of R^1 = Family_open_set RealSpace by TOPMETR:12;

hence A is open by A8, PRE_TOPC:def 2; :: thesis: verum