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 ) } ) )_{1} being non empty strict FMT_Space_Str st

( the carrier of b_{1} = the carrier of T & ( for x being Point of b_{1} holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
; :: thesis: verum

( 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

hence
ex b
deffunc H_{1}( 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_{1}(x) in bool (bool the carrier of T)

A2: for x being Element of T holds f . x = H_{1}(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 A2; :: thesis: verum

end;A1: for x being Element of T holds H

proof

consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that
let x be Element of T; :: thesis: H_{1}(x) in bool (bool the carrier of T)

hence H_{1}(x) in bool (bool the carrier of T)
; :: thesis: verum

end;now :: thesis: for Y being object st Y in { V where V is Subset of T : ( V in the topology of T & x in V ) } holds

Y in bool the carrier of T

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

let Y be object ; :: 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 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: verum

end;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 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: verum

hence H

A2: for x being Element of T holds f . x = H

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 A2; :: thesis: verum

( the carrier of b