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 ( P in Family_open_set M & Family_open_set M = the topology of (TopSpaceMetr M) ) by Th16, PCOMPS_1:33;
hence P is open by PRE_TOPC:def 5; :: thesis: verum