let SUS be non empty axiom_U1 UniformSpaceStr ; :: thesis: for x being Element of the carrier of SUS
for V being Element of the entourages of SUS holds
( Neighborhood (V,x) = V .: {x} & Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )
let x be Element of the carrier of SUS; :: thesis: for V being Element of the entourages of SUS holds
( Neighborhood (V,x) = V .: {x} & Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )
let V be Element of the entourages of SUS; :: thesis: ( Neighborhood (V,x) = V .: {x} & Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )
thus Neighborhood (V,x) = V .: {x} :: thesis: ( Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) )

proof

thus Neighborhood (V,x) c= V .: {x} :: according to XBOOLE_0:def 10 :: thesis: V .: {x} c= Neighborhood (V,x)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Neighborhood (V,x) or t in V .: {x} )
assume t in Neighborhood (V,x) ; :: thesis: t in V .: {x}
then consider y being Element of SUS such that
A3: t = y and
A4: [x,y] in V ;
x in {x} by TARSKI:def 1;
hence t in V .: {x} by A3, A4, RELAT_1:def 13; :: thesis: verum

end;

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in V .: {x} or t in Neighborhood (V,x) )
assume t in V .: {x} ; :: thesis: t in Neighborhood (V,x)
then consider v being object such that
A5: [v,t] in V and
A6: v in {x} by RELAT_1:def 13;
A7: t in the carrier of SUS by A5, ZFMISC_1:87;
[x,t] in V by A5, A6, TARSKI:def 1;
hence t in Neighborhood (V,x) by A7; :: thesis: verum

end;

hence ( Neighborhood (V,x) = rng (V | {x}) & Neighborhood (V,x) = Im (V,x) & Neighborhood (V,x) = Class (V,x) & Neighborhood (V,x) = neighbourhood (,) ) by RELAT_1:115; :: thesis: verum