let PM be MetrStruct ; :: thesis: the carrier of PM in Family_open_set PM
( 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 Th26;
hence the carrier of PM in Family_open_set PM by Def4; :: thesis: verum