ex IT being non empty strict FMT_Space_Str st
( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )

proof

deffunc H₁( set ) -> set = { V where V is Subset of T : ( V in the topology of T & $1 in V ) } ;
A1: for x being Element of T holds H₁(x) in bool (bool the carrier of T)

proof

let x be Element of T; :: thesis: H₁(x) in bool (bool the carrier of T)

now

let Y be set ; :: thesis: ( Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } implies Y in bool the carrier of T )
assume Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } ; :: thesis: Y in bool the carrier of T
then consider V being Subset of T such that
A2: ( V = Y & V in the topology of T & x in V ) ;
thus Y in bool the carrier of T by A2; :: thesis: verum

end;

then { V where V is Subset of T : ( V in the topology of T & x in V ) } c= bool the carrier of T by TARSKI:def 3;
hence H₁(x) in bool (bool the carrier of T) ; :: thesis: verum

end;

consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that
A3: for x being Element of T holds f . x = H₁(x) from FUNCT_2:sch 8(A1);
reconsider IT = FMT_Space_Str(# the carrier of T,f #) as non empty strict FMT_Space_Str ;
take IT ; :: thesis: ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
thus ( the carrier of IT = the carrier of T & ( for x being Point of IT holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) by A3; :: thesis: verum

end;

hence ex b₁ being non empty strict FMT_Space_Str st
( the carrier of b₁ = the carrier of T & ( for x being Point of b₁ holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) ; :: thesis: verum