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