let UT be non empty strict Quasi-UniformSpace; :: thesis: for FMT being non empty strict FMT_Space_Str
for x being Element of FMT st FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) holds
ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y )
let FMT be non empty strict FMT_Space_Str ; :: thesis: for x being Element of FMT st FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) holds
ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y )
let x be Element of FMT; :: thesis: ( FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) implies ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y ) )
assume A1: FMT = FMT_Space_Str(# the carrier of UT,(Neighborhood UT) #) ; :: thesis: ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y )
U_FMT x = the BNbd of FMT . x by FINTOPO2:def 6;
then consider y being Element of UT such that
A2: x = y and
A3: U_FMT x = (Neighborhood UT) . y by A1;
(Neighborhood UT) . y = Neighborhood y by Def5;
hence ex y being Element of UT st
( x = y & U_FMT x = Neighborhood y ) by A2, A3; :: thesis: verum