let r be real number ; :: thesis: for M being triangle MetrStruct
for p being Point of
for P being Subset of st P = Ball p,r holds
P is open
let M be triangle MetrStruct ; :: thesis: for p being Point of
for P being Subset of st P = Ball p,r holds
P is open
let p be Point of ; :: thesis: for P being Subset of st P = Ball p,r holds
P is open
let P be Subset of ; :: 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;
Family_open_set M = the topology of (TopSpaceMetr M) by Th16;
hence P is open by A1, PRE_TOPC:def 5; :: thesis: verum