let PM be MetrStruct ; :: thesis: for x being Element of PM
for r being real number st PM is triangle holds
Ball x,r in Family_open_set PM
let x be Element of PM; :: thesis: for r being real number st PM is triangle holds
Ball x,r in Family_open_set PM
let r be real number ; :: thesis: ( PM is triangle implies Ball x,r in Family_open_set PM )
assume PM is triangle ; :: thesis: Ball x,r in Family_open_set PM
then for y being Element of PM st y in Ball x,r holds
ex p being Real st
( p > 0 & Ball y,p c= Ball x,r ) by Th30;
hence Ball x,r in Family_open_set PM by Def5; :: thesis: verum