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 ;
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