let M be MetrSpace; :: thesis: for B being Subset of (TopSpaceMetr M)
for r being Real
for u being Point of M st B = Ball (u,r) holds
B is open
let B be Subset of (TopSpaceMetr M); :: thesis: for r being Real
for u being Point of M st B = Ball (u,r) holds
B is open
let r be Real; :: thesis: for u being Point of M st B = Ball (u,r) holds
B is open
let u be Point of M; :: thesis: ( B = Ball (u,r) implies B is open )
A1: ( TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) & Ball (u,r) in Family_open_set M ) by PCOMPS_1:29, PCOMPS_1:def 5;
assume B = Ball (u,r) ; :: thesis: B is open
hence B is open by A1, PRE_TOPC:def 2; :: thesis: verum