let USS be non empty axiom_U1 UniformSpaceStr ; :: thesis: for x being Element of the carrier of USS
for V being Element of the entourages of USS holds x in Neighborhood (V,x)
let x be Element of USS; :: thesis: for V being Element of the entourages of USS holds x in Neighborhood (V,x)
let V be Element of the entourages of USS; :: thesis: x in Neighborhood (V,x)
USS is axiom_U1 ;
then A1: id the carrier of USS c= V ;
[x,x] in id the carrier of USS by RELAT_1:def 10;
hence x in Neighborhood (V,x) by A1; :: thesis: verum