let V be RealUnitarySpace; :: thesis: the carrier of V in Family_open_set V
( the carrier of V c= the carrier of V & ( for v being Point of V st v in the carrier of V holds
ex p being Real st
( p > 0 & Ball (v,p) c= the carrier of V ) ) ) by Th34;
hence the carrier of V in Family_open_set V by Def5; :: thesis: verum