let PM be MetrStruct ; :: thesis: for x being Element of PM
for r being Real st PM is triangle holds
Ball (x,r) in Family_open_set PM
let x be Element of PM; :: thesis: for r being Real st PM is triangle holds
Ball (x,r) in Family_open_set PM
let r be Real; :: 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 Th27;
hence Ball (x,r) in Family_open_set PM by Def4; :: thesis: verum