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:

now :: thesis:

let Y be object ; :: thesis:
assume Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } ; :: thesis:
then ex V being Subset of T st
( V = Y & V in the topology of T & x in V ) ;
hence Y in bool the carrier of T ; :: thesis:

end;

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

end;

consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that
A2: 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:
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 A2; :: thesis:

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: