:: deftheorem Def4 defines Family_open_set PCOMPS_1:def 4 :
for PM being MetrStruct
for b₂ being Subset-Family of PM holds
( b₂ = Family_open_set PM iff for V being Subset of PM holds
( V in b₂ iff for x being Element of PM st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) );