:: A Case Study of Transport Urysohn's Lemma from TopSpace Defined with Open Sets to TopSpace Defined with Neighborhoods
:: by Roland Coghetto
::
:: Copyright (c) 2020-2021 Association of Mizar Users

theorem Th1: :: FINTOPO8:1
for T being TopSpace
for A, B being Subset of T st A misses B holds
Int A misses Int B
proof end;

definition end;

notation
let X be non empty TopSpace;
synonym Top2NTop X for TopSpace2FMT X;
end;

notation
let X be FMT_TopSpace;
synonym NTop2Top X for FMT2TopSpace X;
end;

Lm1: for TX being non empty TopSpace
for O being open Subset of TX holds O is open Subset of (Top2NTop TX)

proof end;

Lm2: for NTX being NTopSpace holds
( [#] NTX is open & {} NTX is open )

proof end;

registration
let NTX be NTopSpace;
cluster [#] NTX -> open ;
coherence
[#] NTX is open
by Lm2;
cluster {} NTX -> open ;
coherence
{} NTX is open
by Lm2;
end;

definition
let NTX be non empty strict U_FMT_filter FMT_Space_Str ;
let x be Element of NTX;
:: original: U_FMT
redefine func U_FMT x -> Filter of the carrier of NTX;
coherence
U_FMT x is Filter of the carrier of NTX
by FINTOPO7:def 2;
end;

definition
let NTX be non empty strict U_FMT_filter FMT_Space_Str ;
let F be Filter of the carrier of NTX;
func lim_filter F -> Subset of NTX equals :: FINTOPO8:def 1
{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;
correctness
coherence
{ x where x is Point of NTX : F is_filter-finer_than U_FMT x } is Subset of NTX
;
proof end;
end;

:: deftheorem defines lim_filter FINTOPO8:def 1 :
for NTX being non empty strict U_FMT_filter FMT_Space_Str
for F being Filter of the carrier of NTX holds lim_filter F = { x where x is Point of NTX : F is_filter-finer_than U_FMT x } ;

definition
let NTX, NTY be non empty strict U_FMT_filter FMT_Space_Str ;
let f be Function of NTX,NTY;
let F be Filter of the carrier of NTX;
func lim_filter (f,F) -> Subset of NTY equals :: FINTOPO8:def 2
lim_filter (filter_image (f,F));
coherence
lim_filter (filter_image (f,F)) is Subset of NTY
;
end;

:: deftheorem defines lim_filter FINTOPO8:def 2 :
for NTX, NTY being non empty strict U_FMT_filter FMT_Space_Str
for f being Function of NTX,NTY
for F being Filter of the carrier of NTX holds lim_filter (f,F) = lim_filter (filter_image (f,F));

definition
let NT be NTopSpace;
let A be Subset of NT;
let x be Point of NT;
pred x is_interior_point_of A means :: FINTOPO8:def 3
A is a_neighborhood of x;
end;

:: deftheorem defines is_interior_point_of FINTOPO8:def 3 :
for NT being NTopSpace
for A being Subset of NT
for x being Point of NT holds
( x is_interior_point_of A iff A is a_neighborhood of x );

definition
let NT be NTopSpace;
let A be Subset of NT;
let x be Point of NT;
pred x is_adherent_point_of A means :: FINTOPO8:def 4
for V being Element of U_FMT x holds V meets A;
end;

:: deftheorem defines is_adherent_point_of FINTOPO8:def 4 :
for NT being NTopSpace
for A being Subset of NT
for x being Point of NT holds
( x is_adherent_point_of A iff for V being Element of U_FMT x holds V meets A );

definition
let NT be NTopSpace;
let A be Subset of NT;
func Int A -> Subset of NT equals :: FINTOPO8:def 5
{ x where x is Point of NT : x is_interior_point_of A } ;
coherence
{ x where x is Point of NT : x is_interior_point_of A } is Subset of NT
proof end;
end;

:: deftheorem defines Int FINTOPO8:def 5 :
for NT being NTopSpace
for A being Subset of NT holds Int A = { x where x is Point of NT : x is_interior_point_of A } ;

definition
let NTX, NTY be NTopSpace;
let f be Function of NTX,NTY;
let x be Point of NTX;
pred f is_continuous_at x means :: FINTOPO8:def 6
for F being Filter of the carrier of NTX st x in lim_filter F holds
f . x in lim_filter (f,F);
end;

:: deftheorem defines is_continuous_at FINTOPO8:def 6 :
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY
for x being Point of NTX holds
( f is_continuous_at x iff for F being Filter of the carrier of NTX st x in lim_filter F holds
f . x in lim_filter (f,F) );

definition
let NTX, NTY be NTopSpace;
let f be Function of NTX,NTY;
attr f is continuous means :: FINTOPO8:def 7
for x being Point of NTX holds f is_continuous_at x;
end;

:: deftheorem defines continuous FINTOPO8:def 7 :
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY holds
( f is continuous iff for x being Point of NTX holds f is_continuous_at x );

Lm3: for NTX, NTY being NTopSpace
for a being Point of NTY holds NTX --> a is continuous

proof end;

registration
let NTX, NTY be NTopSpace;
cluster non empty V7() V10( the carrier of NTX) V11( the carrier of NTY) Function-like V27( the carrier of NTX) V31( the carrier of NTX, the carrier of NTY) continuous for Element of bool [: the carrier of NTX, the carrier of NTY:];
existence
ex b1 being Function of NTX,NTY st b1 is continuous
proof end;
end;

Lm4: for NT being NTopSpace
for A being Subset of NT
for x being Point of NT holds
( x is_interior_point_of A iff ex O being open Subset of NT st
( x in O & O c= A ) )

proof end;

Lm5: for NT being NTopSpace
for A being Subset of NT holds Int A = union { O where O is open Subset of NT : O c= A }

proof end;

registration
let NT be NTopSpace;
let A be Subset of NT;
cluster Int A -> open ;
coherence
Int A is open
proof end;
end;

definition
let NT be NTopSpace;
let A be Subset of NT;
func Cl A -> Subset of NT equals :: FINTOPO8:def 8
{ x where x is Point of NT : x is_adherent_point_of A } ;
coherence
{ x where x is Point of NT : x is_adherent_point_of A } is Subset of NT
proof end;
end;

:: deftheorem defines Cl FINTOPO8:def 8 :
for NT being NTopSpace
for A being Subset of NT holds Cl A = { x where x is Point of NT : x is_adherent_point_of A } ;

definition
let NTX be NTopSpace;
let A be Subset of NTX;
attr A is closed means :Def9: :: FINTOPO8:def 9
([#] NTX) \ A is open Subset of NTX;
end;

:: deftheorem Def9 defines closed FINTOPO8:def 9 :
for NTX being NTopSpace
for A being Subset of NTX holds
( A is closed iff ([#] NTX) \ A is open Subset of NTX );

registration
let NTX be NTopSpace;
cluster closed for Element of bool the carrier of NTX;
existence
ex b1 being Subset of NTX st b1 is closed
proof end;
end;

registration
let NTX be NTopSpace;
cluster [#] NTX -> closed for Subset of NTX;
coherence
for b1 being Subset of NTX st b1 = [#] NTX holds
b1 is closed
proof end;
cluster {} NTX -> closed for Subset of NTX;
coherence
for b1 being Subset of NTX st b1 = {} NTX holds
b1 is closed
;
end;

registration
let NTX be NTopSpace;
cluster non empty closed for Element of bool the carrier of NTX;
existence
ex b1 being Subset of NTX st
( not b1 is empty & b1 is closed )
proof end;
end;

definition
let S, T be non empty TopSpace;
let f be Function of S,T;
func Top2NTop f -> Function of (),() equals :: FINTOPO8:def 10
f;
coherence
f is Function of (),()
proof end;
end;

:: deftheorem defines Top2NTop FINTOPO8:def 10 :
for S, T being non empty TopSpace
for f being Function of S,T holds Top2NTop f = f;

Lm6: for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
( A is open iff B is closed )

proof end;

Lm7: for TX being non empty TopSpace
for F being closed Subset of TX holds F is closed Subset of (Top2NTop TX)

proof end;

Lm8: for NT being NTopSpace
for A, B being Subset of NT st A = ([#] NT) \ B holds
( A is open iff B is closed )

;

Lm9: for NTX being NTopSpace
for O being open Subset of NTX holds O is open Subset of (NTop2Top NTX)

proof end;

Lm10: for NTX being NTopSpace
for F being closed Subset of NTX holds F is closed Subset of (NTop2Top NTX)

proof end;

Lm11: for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V

proof end;

Lm12: for NTX, NTY being NTopSpace
for A being Subset of NTX
for B being Subset of NTY
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of A & y = f . x & B = f .: A holds

proof end;

Lm13: for NTX, NTY being NTopSpace
for A being Subset of NTX
for f being continuous Function of NTX,NTY holds f .: (Cl A) c= Cl (f .: A)

proof end;

Lm14: for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Cl A) = Int B

proof end;

Lm15: for NT being NTopSpace
for A being Subset of NT holds Int A c= A

proof end;

Lm16: for NT being NTopSpace
for A being Subset of NT
for B being open Subset of NT st B c= A holds
B c= Int A

proof end;

Lm17: for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Int A c= Int B

proof end;

Lm18: for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Cl A c= Cl B

proof end;

Lm19: for NT being NTopSpace
for A being Subset of NT holds
( A is open iff Int A = A )

proof end;

Lm20: for NTX being NTopSpace
for A being closed Subset of NTX holds Cl A = A

proof end;

Lm21: for NT being NTopSpace
for A being Subset of NT holds A c= Cl A

proof end;

Lm22: for NTX being NTopSpace
for A being Subset of NTX st Cl A = A holds
A is closed Subset of NTX

proof end;

Lm23: for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for A being Subset of NTX holds f .: (Cl A) c= Cl (f .: A) ) holds
for S being closed Subset of NTY holds f " S is closed Subset of NTX

proof end;

Lm24: for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for S being closed Subset of NTY holds f " S is closed Subset of NTX ) holds
for S being open Subset of NTY holds f " S is open Subset of NTX

proof end;

Lm25: for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st y = f . x & ( for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) holds
f is_continuous_at x

proof end;

Lm26: for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for S being open Subset of NTY holds f " S is open Subset of NTX ) holds
f is continuous

proof end;

Lm27: for NTX, NTY being NTopSpace
for f being Function of NTX,NTY holds
( f is continuous iff for O being closed Subset of NTY holds f " O is closed Subset of NTX )

proof end;

definition
let TX be non empty TopSpace;
let TY be non empty strict TopSpace;
let f be continuous Function of TX,TY;
:: original: Top2NTop
redefine func Top2NTop f -> continuous Function of (Top2NTop TX),(Top2NTop TY) equals :: FINTOPO8:def 11
f;
correctness
coherence
Top2NTop f is continuous Function of (Top2NTop TX),(Top2NTop TY)
;
compatibility
for b1 being continuous Function of (Top2NTop TX),(Top2NTop TY) holds
( b1 = Top2NTop f iff b1 = f )
;
proof end;
end;

:: deftheorem defines Top2NTop FINTOPO8:def 11 :
for TX being non empty TopSpace
for TY being non empty strict TopSpace
for f being continuous Function of TX,TY holds Top2NTop f = f;

definition
let NT be NTopSpace;
attr NT is T_2 means :Def12: :: FINTOPO8:def 12
for F being Filter of the carrier of NT holds lim_filter F is trivial ;
end;

:: deftheorem Def12 defines T_2 FINTOPO8:def 12 :
for NT being NTopSpace holds
( NT is T_2 iff for F being Filter of the carrier of NT holds lim_filter F is trivial );

registration
existence
ex b1 being NTopSpace st b1 is T_2
proof end;
end;

definition
let NT be NTopSpace;
attr NT is normal means :Def13: :: FINTOPO8:def 13
for A, B being closed Subset of NT st A misses B holds
ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W;
end;

:: deftheorem Def13 defines normal FINTOPO8:def 13 :
for NT being NTopSpace holds
( NT is normal iff for A, B being closed Subset of NT st A misses B holds
ex V being a_neighborhood of A ex W being a_neighborhood of B st V misses W );

Lm28: for T being non empty T_2 TopSpace holds Top2NTop T is T_2 NTopSpace
proof end;

Lm29: for NTX being NTopSpace
for A being closed Subset of NTX holds A is closed Subset of (NTop2Top NTX)

proof end;

definition
let NT be NTopSpace;
let x be Point of NT;
func NTop2Top x -> Point of (NTop2Top NT) equals :: FINTOPO8:def 14
x;
coherence
x is Point of (NTop2Top NT)
by FINTOPO7:def 16;
end;

:: deftheorem defines NTop2Top FINTOPO8:def 14 :
for NT being NTopSpace
for x being Point of NT holds NTop2Top x = x;

definition
let T be non empty TopSpace;
let x be Point of T;
func Top2NTop x -> Point of () equals :: FINTOPO8:def 15
x;
coherence
x is Point of ()
by FINTOPO7:def 15;
end;

:: deftheorem defines Top2NTop FINTOPO8:def 15 :
for T being non empty TopSpace
for x being Point of T holds Top2NTop x = x;

definition
let NT be NTopSpace;
let S be Subset of NT;
func NTop2Top S -> Subset of (NTop2Top NT) equals :: FINTOPO8:def 16
S;
coherence
S is Subset of (NTop2Top NT)
by FINTOPO7:def 16;
end;

:: deftheorem defines NTop2Top FINTOPO8:def 16 :
for NT being NTopSpace
for S being Subset of NT holds NTop2Top S = S;

definition
let T be non empty TopSpace;
let S be Subset of T;
func Top2NTop S -> Subset of () equals :: FINTOPO8:def 17
S;
coherence
S is Subset of ()
by FINTOPO7:def 15;
end;

:: deftheorem defines Top2NTop FINTOPO8:def 17 :
for T being non empty TopSpace
for S being Subset of T holds Top2NTop S = S;

Lm30: for T being non empty strict TopSpace
for A being Subset of T holds Int A = Int ()

proof end;

Lm31: for T being non empty strict TopSpace
for A, B being Subset of T st A is a_neighborhood of B holds
Top2NTop A is a_neighborhood of Top2NTop B

proof end;

registration
existence
ex b1 being NTopSpace st
( not b1 is empty & b1 is normal )
proof end;
end;

definition
let TX, TY be NTopSpace;
let f be Function of TX,TY;
func NTop2Top f -> Function of (NTop2Top TX),(NTop2Top TY) equals :: FINTOPO8:def 18
f;
coherence
f is Function of (NTop2Top TX),(NTop2Top TY)
proof end;
end;

:: deftheorem defines NTop2Top FINTOPO8:def 18 :
for TX, TY being NTopSpace
for f being Function of TX,TY holds NTop2Top f = f;

definition
coherence ;
end;

:: deftheorem defines FMT_R^1 FINTOPO8:def 19 :

theorem :: FINTOPO8:2

registration
coherence
proof end;
end;

theorem :: FINTOPO8:3
for NT being NTopSpace
for O being open Subset of NT holds O is open Subset of (NTop2Top NT) by Lm9;

theorem :: FINTOPO8:4
for NT being NTopSpace
for A being Subset of NT holds A is Subset of (NTop2Top NT) by FINTOPO7:def 16;

theorem :: FINTOPO8:5
for NT being NTopSpace holds
( [#] NT is open & {} NT is open ) ;

theorem :: FINTOPO8:6
for NT, NTY being NTopSpace
for y being Point of NTY holds NT --> y is continuous by Lm3;

theorem :: FINTOPO8:7
for NT being NTopSpace
for A being Subset of NT
for a being Point of NT holds
( a is_interior_point_of A iff ex O being open Subset of NT st
( a in O & O c= A ) ) by Lm4;

theorem :: FINTOPO8:8
for NT being NTopSpace
for O being open Subset of NT
for a being Point of NT st a in O holds
a is_interior_point_of O by Lm4;

theorem :: FINTOPO8:9
for NT being NTopSpace
for A being Subset of NT holds Int A = union { O where O is open Subset of NT : O c= A } by Lm5;

theorem :: FINTOPO8:10
for NT being NTopSpace
for A being Subset of NT holds Int A c= A by Lm15;

theorem :: FINTOPO8:11
for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Int A c= Int B by Lm17;

theorem Th12: :: FINTOPO8:12
for NT being NTopSpace
for A being Subset of NT holds
( A is open iff Int A = A )
proof end;

theorem :: FINTOPO8:13
for NT being NTopSpace
for A being Subset of NT holds Int A = Int (Int A) by Th12;

theorem Th14: :: FINTOPO8:14
for NT being NTopSpace
for A being Subset of NT
for x being Point of NT st A is a_neighborhood of x holds
Int A is open a_neighborhood of x
proof end;

theorem :: FINTOPO8:15
for NTX, NTY being NTopSpace
for x being Point of NTX
for f being Function of NTX,NTY holds filter_image (f,()) = { M where M is Subset of NTY : f " M in U_FMT x } by CARDFIL2:def 13;

theorem :: FINTOPO8:16
for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & y = f . x holds
for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V by Lm11;

theorem :: FINTOPO8:17
for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st y = f . x & ( for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) holds
f is_continuous_at x by Lm25;

theorem :: FINTOPO8:18
for NTX, NTY being NTopSpace
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st y = f . x holds
( f is_continuous_at x iff for V being Element of U_FMT y ex W being Element of U_FMT x st f .: W c= V ) by ;

theorem :: FINTOPO8:19
for NTX, NTY being NTopSpace
for XA being Subset of NTX
for YB being Subset of NTY
for x being Point of NTX
for y being Point of NTY
for f being Function of NTX,NTY st f is_continuous_at x & x is_adherent_point_of XA & y = f . x & YB = f .: XA holds

theorem :: FINTOPO8:20
for NTX, NTY being NTopSpace
for XA being Subset of NTX
for fc being continuous Function of NTX,NTY holds fc .: (Cl XA) c= Cl (fc .: XA) by Lm13;

theorem :: FINTOPO8:21
for NT being NTopSpace
for A being closed Subset of NT holds A is closed Subset of (NTop2Top NT) by Lm29;

theorem :: FINTOPO8:22
for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Cl A) = Int B by Lm14;

theorem :: FINTOPO8:23
for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
([#] NT) \ (Int A) = Cl B
proof end;

theorem :: FINTOPO8:24
for NT being NTopSpace
for A being Subset of NT holds A c= Cl A by Lm21;

theorem :: FINTOPO8:25
for NT being NTopSpace
for A being Subset of NT holds
( A is closed iff Cl A = A ) by ;

theorem :: FINTOPO8:26
for NT being NTopSpace
for A, B being Subset of NT st A c= B holds
Cl A c= Cl B by Lm18;

theorem :: FINTOPO8:27
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for XA being Subset of NTX holds f .: (Cl XA) c= Cl (f .: XA) ) holds
for S being closed Subset of NTY holds f " S is closed Subset of NTX by Lm23;

theorem :: FINTOPO8:28
for NT being NTopSpace
for A, B being Subset of NT st B = ([#] NT) \ A holds
( A is open iff B is closed ) by Lm6;

theorem :: FINTOPO8:29
for NT being NTopSpace
for A, B being Subset of NT st A = ([#] NT) \ B holds
( A is open iff B is closed ) ;

theorem :: FINTOPO8:30
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for S being closed Subset of NTY holds f " S is closed Subset of NTX ) holds
for S being open Subset of NTY holds f " S is open Subset of NTX by Lm24;

theorem :: FINTOPO8:31
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY st ( for S being open Subset of NTY holds f " S is open Subset of NTX ) holds
f is continuous by Lm26;

theorem :: FINTOPO8:32
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY holds
( f is continuous iff for O being open Subset of NTY holds f " O is open Subset of NTX )
proof end;

theorem :: FINTOPO8:33
for NTX, NTY being NTopSpace
for f being Function of NTX,NTY holds
( f is continuous iff for O being closed Subset of NTY holds f " O is closed Subset of NTX ) by Lm27;

theorem Th34: :: FINTOPO8:34
for NT being NTopSpace
for A being Subset of NT holds Int A = Int ()
proof end;

theorem :: FINTOPO8:35
for NT being NTopSpace
for A being Subset of NT
for a being Point of NT st A is a_neighborhood of a holds
NTop2Top A is a_neighborhood of NTop2Top a
proof end;

theorem Th36: :: FINTOPO8:36
for NT being NTopSpace
for A, B being Subset of NT st A is a_neighborhood of B holds
NTop2Top A is a_neighborhood of NTop2Top B
proof end;

theorem :: FINTOPO8:37
for NT being NTopSpace
for A, B being Subset of NT st A misses B holds
NTop2Top A misses NTop2Top B ;

theorem :: FINTOPO8:38
for NT being NTopSpace
for A, B being Subset of NT st A misses B holds
Int A misses Int B
proof end;

theorem Th39: :: FINTOPO8:39
for NT being T_2 NTopSpace
for x, y being Point of NT st x <> y holds
ex Vx being Element of U_FMT x ex Vy being Element of U_FMT y st Vx misses Vy
proof end;

theorem :: FINTOPO8:40
for NT being T_2 NTopSpace holds NTop2Top NT is non empty strict T_2 TopSpace
proof end;

theorem Th41: :: FINTOPO8:41
for NT being normal NTopSpace holds NTop2Top NT is normal
proof end;

registration
let NT be normal NTopSpace;
coherence
NTop2Top NT is normal
by Th41;
end;

theorem :: FINTOPO8:42
for T being non empty TopSpace
for A being Subset of T holds A is Subset of () by FINTOPO7:def 15;

theorem :: FINTOPO8:43
for T being non empty TopSpace
for F being closed Subset of T holds F is closed Subset of () by Lm7;

theorem :: FINTOPO8:44
for T being non empty TopSpace
for O being open Subset of T holds O is open Subset of () by Lm1;

theorem :: FINTOPO8:45
for T being non empty TopSpace
for A, B being Subset of T st A misses B holds
Top2NTop A misses Top2NTop B ;

theorem :: FINTOPO8:46
for T being non empty T_2 TopSpace holds Top2NTop T is T_2 NTopSpace by Lm28;

theorem :: FINTOPO8:47
for T being non empty strict TopSpace
for A being Subset of T holds Int A = Int () by Lm30;

theorem :: FINTOPO8:48
for T being non empty strict TopSpace
for A, B being Subset of T st A is a_neighborhood of B holds
Top2NTop A is a_neighborhood of Top2NTop B by Lm31;

theorem :: FINTOPO8:49
for T being non empty strict TopSpace
for A being Subset of T
for x being Point of T st A is a_neighborhood of x holds
Top2NTop A is a_neighborhood of Top2NTop x
proof end;

theorem TH: :: FINTOPO8:50
for T being non empty strict normal TopSpace holds Top2NTop T is normal
proof end;

registration
let T be non empty strict normal TopSpace;
coherence by TH;
end;

theorem :: FINTOPO8:51

theorem Th52: :: FINTOPO8:52

theorem :: FINTOPO8:53
for NT being NTopSpace
for f being Function of NT,FMT_R^1 holds NTop2Top f is Function of (NTop2Top NT),R^1 by FINTOPO7:24;

theorem :: FINTOPO8:54
for T being non empty TopSpace
for f being Function of T,R^1 holds Top2NTop f is Function of (),() ;

theorem Th55: :: FINTOPO8:55
for A being Subset of FMT_R^1 holds
( A is open iff for x being Real st x in A holds
ex r being Real st
( r > 0 & ].(x - r),(x + r).[ c= A ) )
proof end;

theorem :: FINTOPO8:56
{ ].a,b.[ where a, b is Real : a < b } is Basis of R^1 by TOPGEN_5:72;

theorem Th57: :: FINTOPO8:57
{ ].a,b.[ where a, b is Real : a < b } is Basis of FMT_R^1
proof end;

theorem Th58: :: FINTOPO8:58
for x being Point of FMT_R^1
for r being Real st r > 0 holds
].(x - r),(x + r).[ is a_neighborhood of x
proof end;

theorem :: FINTOPO8:59
for x being object holds
( x is Point of FMT_R^1 iff x is Point of RealSpace ) by ;

theorem :: FINTOPO8:60
for x being Point of FMT_R^1
for y being Point of RealSpace
for r being Real st x = y holds
Ball (y,r) = ].(x - r),(x + r).[ by FRECHET:7;

theorem Th61: :: FINTOPO8:61
for x being Point of FMT_R^1
for y being Point of RealSpace
for r being Real st x = y & r > 0 holds
Ball (y,r) is a_neighborhood of x
proof end;

theorem :: FINTOPO8:62
for x being Point of FMT_R^1
for z being Point of st x = z holds
Balls z is Subset-Family of FMT_R^1 by ;

theorem :: FINTOPO8:63
for x being Point of FMT_R^1
for z being Point of
for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds
<.SF.] = U_FMT x
proof end;

definition
func gen_NS_R^1 -> Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) means :Def20: :: FINTOPO8:def 20
for r being Real ex x being Point of st
( x = r & it . r = Balls x );
existence
ex b1 being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st
for r being Real ex x being Point of st
( x = r & b1 . r = Balls x )
proof end;
uniqueness
for b1, b2 being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) st ( for r being Real ex x being Point of st
( x = r & b1 . r = Balls x ) ) & ( for r being Real ex x being Point of st
( x = r & b2 . r = Balls x ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def20 defines gen_NS_R^1 FINTOPO8:def 20 :
for b1 being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) holds
( b1 = gen_NS_R^1 iff for r being Real ex x being Point of st
( x = r & b1 . r = Balls x ) );

definition
func gen_R^1 -> non empty strict FMT_Space_Str equals :: FINTOPO8:def 21
FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);
coherence
FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #) is non empty strict FMT_Space_Str
;
end;

:: deftheorem defines gen_R^1 FINTOPO8:def 21 :
gen_R^1 = FMT_Space_Str(# the carrier of FMT_R^1,gen_NS_R^1 #);

theorem Th64: :: FINTOPO8:64

theorem Th65: :: FINTOPO8:65
for x being Element of gen_R^1 ex y being Point of st
( x = y & U_FMT x = Balls y )
proof end;

theorem :: FINTOPO8:66

theorem :: FINTOPO8:67
proof end;

theorem :: FINTOPO8:68
for NT being normal NTopSpace
for A, B being closed Subset of NT st A misses B holds
ex F being Function of NT,FMT_R^1 st
( F is continuous & ( for x being Point of NT holds
( 0 <= F . x & F . x <= 1 & ( x in A implies F . x = 0 ) & ( x in B implies F . x = 1 ) ) ) )
proof end;