let V be RealUnitarySpace; :: thesis: the carrier of V in Family_open_set V
A1: 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 A1, Def5; :: thesis: verum