let S be RealNormSpace; :: thesis: for X being Subset of S st X is open holds

for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

let X be Subset of S; :: thesis: ( X is open implies for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )

assume A1: X is open ; :: thesis: for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

let r be Point of S; :: thesis: ( r in X implies ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )

assume r in X ; :: thesis: ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

then consider N being Neighbourhood of r such that

A2: N c= X by A1, Th2;

consider g being Real such that

A3: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= N ) by NFCONT_1:def 1;

take g ; :: thesis: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

thus ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) by A2, A3; :: thesis: verum

for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

let X be Subset of S; :: thesis: ( X is open implies for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )

assume A1: X is open ; :: thesis: for r being Point of S st r in X holds

ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

let r be Point of S; :: thesis: ( r in X implies ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) )

assume r in X ; :: thesis: ex g being Real st

( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

then consider N being Neighbourhood of r such that

A2: N c= X by A1, Th2;

consider g being Real such that

A3: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= N ) by NFCONT_1:def 1;

take g ; :: thesis: ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X )

thus ( 0 < g & { y where y is Point of S : ||.(y - r).|| < g } c= X ) by A2, A3; :: thesis: verum