let PM be MetrStruct ; :: thesis: the carrier of PM in Family_open_set PM
A1: the carrier of PM c= the carrier of PM ;
for y being Element of PM st y in the carrier of PM holds
ex p being Real st
( p > 0 & Ball y,p c= the carrier of PM ) by Th29;
hence the carrier of PM in Family_open_set PM by A1, Def5; :: thesis: verum