let r be real number ; :: thesis: for M being triangle MetrStruct
for p being Point of M
for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
let M be triangle MetrStruct ; :: thesis: for p being Point of M
for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
let p be Point of M; :: thesis: for P being Subset of (TopSpaceMetr M) st P = Ball (p,r) holds
P is open
let P be Subset of (TopSpaceMetr M); :: thesis: ( P = Ball (p,r) implies P is open )
assume P = Ball (p,r) ; :: thesis: P is open
then A1: P in Family_open_set M by PCOMPS_1:33;
thus P is open by A1, PRE_TOPC:def 5; :: thesis: verum