let US be non empty UniformSpace; :: thesis: for S being Subset of (FMT_induced_by US) holds
( S is open iff S in Family_open_set (FMT_induced_by US) )
let S be Subset of (FMT_induced_by US); :: thesis: ( S is open iff S in Family_open_set (FMT_induced_by US) )
thus ( S is open implies S in Family_open_set (FMT_induced_by US) ) ; :: thesis: ( S in Family_open_set (FMT_induced_by US) implies S is open )
assume S in Family_open_set (FMT_induced_by US) ; :: thesis: S is open
then ex O being open Subset of (FMT_induced_by US) st S = O ;
hence S is open ; :: thesis: verum