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

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