let S be RealUnitarySpace; :: thesis:
set PM = MetricSpaceNorm (RUSp2RNSp S);
set FPM = Family_open_set (MetricSpaceNorm (RUSp2RNSp S));
for M being Subset of S holds
( M in Family_open_set (MetricSpaceNorm (RUSp2RNSp S)) iff for x being Point of S st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) )

let M be Subset of S; :: thesis:
reconsider N = M as Subset of (MetricSpaceNorm (RUSp2RNSp S)) ;

let x be Point of S; :: thesis:
assume A2: x in M ; :: thesis:
reconsider y = x as Element of (MetricSpaceNorm (RUSp2RNSp S)) ;
consider r being Real such that
A3: ( r > 0 & Ball (y,r) c= N ) by A2, A1, PCOMPS_1:def 4;
take r ; :: thesis:
thus 0 < r by A3; :: thesis:
thus Ball (x,r) c= M by A3, Th13; :: thesis:

end;

assume A4: for x being Point of S st x in M holds
ex r being Real st
( r > 0 & Ball (x,r) c= M ) ; :: thesis:
for y being Element of (MetricSpaceNorm (RUSp2RNSp S)) st y in N holds
ex r being Real st
( r > 0 & Ball (y,r) c= N )

let y be Element of (MetricSpaceNorm (RUSp2RNSp S)); :: thesis:
assume A5: y in N ; :: thesis:
reconsider x = y as Point of S ;
consider r being Real such that
A6: ( r > 0 & Ball (x,r) c= M ) by A4, A5;
take r ; :: thesis:
thus 0 < r by A6; :: thesis:
thus Ball (y,r) c= N by A6, Th13; :: thesis:

end;

end;