set S = the carrier of ET;
take the carrier of ET ; :: thesis: ( the carrier of ET is Subset of ET & the carrier of ET is a_neighborhood of x & the carrier of ET is open )
A1: the carrier of ET in U_FMT x by Th6;
then reconsider S = the carrier of ET as Subset of ET ;
S is open by Th6;
hence ( the carrier of ET is Subset of ET & the carrier of ET is a_neighborhood of x & the carrier of ET is open ) by A1, Def5; :: thesis: verum