set SN = Neighborhood x;
not the entourages of USS is empty ;
then consider V0 being object such that
A2: V0 in the entourages of USS ;
reconsider V1 = V0 as Element of the entourages of USS by A2;
Neighborhood (V1,x) in Neighborhood x ;
hence not Neighborhood x is empty ; :: thesis: verum