set S = the carrier of ET;

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of ET ;

for x being Element of ET st x in A holds

S in U_FMT x by Th6;

then A1: S is a_neighborhood of A by Def6;

S is open by Th6;

hence ex b_{1} being a_neighborhood of A st b_{1} is open
by A1; :: thesis: verum

the carrier of ET c= the carrier of ET ;

then reconsider S = the carrier of ET as Subset of ET ;

for x being Element of ET st x in A holds

S in U_FMT x by Th6;

then A1: S is a_neighborhood of A by Def6;

S is open by Th6;

hence ex b