let US be non empty UniformSpace; :: thesis: for S being Subset of (FMT_induced_by US) holds
( S is open iff for x being Element of US st x in S holds
S in Neighborhood x )
let S be Subset of (FMT_induced_by US); :: thesis: ( S is open iff for x being Element of US st x in S holds
S in Neighborhood x )
hereby :: thesis: ( ( for x being Element of US st x in S holds
S in Neighborhood x ) implies S is open )
assume A1: S is open ; :: thesis: for x being Element of US st x in S holds
S in Neighborhood x
hereby :: thesis: verum
let x be Element of US; :: thesis: ( x in S implies S in Neighborhood x )
assume A2: x in S ; :: thesis: S in Neighborhood x
reconsider x1 = x as Element of (FMT_induced_by US) ;
U_FMT x1 = Neighborhood x by UNIFORM2:def 14;
hence S in Neighborhood x by A1, A2; :: thesis: verum
end;
end;
assume A3: for x being Element of US st x in S holds
S in Neighborhood x ; :: thesis: S is open
now :: thesis: for x being Element of (FMT_induced_by US) st x in S holds
S in U_FMT x
let x be Element of (FMT_induced_by US); :: thesis: ( x in S implies S in U_FMT x )
assume A4: x in S ; :: thesis: S in U_FMT x
consider y being Element of US such that
A5: x = y and
A6: U_FMT x = (Neighborhood US) . y ;
U_FMT x = Neighborhood y by A6, UNIFORM2:def 14;
hence S in U_FMT x by A3, A4, A5; :: thesis: verum
end;
hence S is open ; :: thesis: verum