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