let T be non empty TopSpace; :: thesis: ex ET being FMT_TopSpace st

( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T )

ex ET being non empty strict FMT_Space_Str st

( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

A56: the carrier of T = the carrier of ET and

( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local ) and

A57: ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) ;

consider TT being FMT_TopSpace such that

A58: TT = ET and

Family_open_set TT = the topology of T by A57;

take TT ; :: thesis: ( the carrier of T = the carrier of TT & Family_open_set TT = the topology of T )

thus ( the carrier of T = the carrier of TT & Family_open_set TT = the topology of T ) by A56, A57, A58; :: thesis: verum

( the carrier of T = the carrier of ET & Family_open_set ET = the topology of T )

ex ET being non empty strict FMT_Space_Str st

( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

proof

then consider ET being non empty strict FMT_Space_Str such that
deffunc H_{1}( object ) -> set = { O where O is Element of the topology of T : $1 in O } ;

A1: for x being object st x in the carrier of T holds

H_{1}(x) in bool (bool the carrier of T)

for x being object st x in the carrier of T holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A1);

then consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that

A5: for x being object st x in the carrier of T holds

f . x = H_{1}(x)
;

reconsider TMP = FMT_Space_Str(# the carrier of T,f #) as non empty strict FMT_Space_Str ;

A6: for t being Element of TMP holds not U_FMT t is empty

take ET ; :: thesis: ( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

thus ET is U_FMT_filter by A7, Th8; :: thesis: ( ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

thus A18: ET is U_FMT_with_point :: thesis: ( ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

( TT = ET & Family_open_set TT = the topology of T ) )

( TT = ET & Family_open_set TT = the topology of T )

ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T )

( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum

end;A1: for x being object st x in the carrier of T holds

H

proof

ex f being Function of the carrier of T,(bool (bool the carrier of T)) st
let x be object ; :: thesis: ( x in the carrier of T implies H_{1}(x) in bool (bool the carrier of T) )

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

reconsider x = x as Element of T by A2;

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

end;assume A2: x in the carrier of T ; :: thesis: H

reconsider x = x as Element of T by A2;

H

proof

hence
H
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in H_{1}(x) or t in bool the carrier of T )

assume A3: t in H_{1}(x)
; :: thesis: t in bool the carrier of T

consider O1 being Element of the topology of T such that

A4: t = O1 and

x in O1 by A3;

thus t in bool the carrier of T by A4; :: thesis: verum

end;assume A3: t in H

consider O1 being Element of the topology of T such that

A4: t = O1 and

x in O1 by A3;

thus t in bool the carrier of T by A4; :: thesis: verum

for x being object st x in the carrier of T holds

f . x = H

then consider f being Function of the carrier of T,(bool (bool the carrier of T)) such that

A5: for x being object st x in the carrier of T holds

f . x = H

reconsider TMP = FMT_Space_Str(# the carrier of T,f #) as non empty strict FMT_Space_Str ;

A6: for t being Element of TMP holds not U_FMT t is empty

proof

A7:
TMP is U_FMT_filter_base
let t be Element of TMP; :: thesis: not U_FMT t is empty

take TT = the carrier of T; :: according to XBOOLE_0:def 1 :: thesis: TT in U_FMT t

TT in the topology of T by PRE_TOPC:def 1;

then TT in H_{1}(t)
;

hence TT in U_FMT t by A5; :: thesis: verum

end;take TT = the carrier of T; :: according to XBOOLE_0:def 1 :: thesis: TT in U_FMT t

TT in the topology of T by PRE_TOPC:def 1;

then TT in H

hence TT in U_FMT t by A5; :: thesis: verum

proof

reconsider ET = gen_filter TMP as non empty strict FMT_Space_Str ;
for x being Element of the carrier of TMP holds

( not U_FMT x is empty & U_FMT x is with_non-empty_elements & ( for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2 ) )

( not U_FMT x is empty & U_FMT x is with_non-empty_elements & U_FMT x is quasi_basis ) ;

hence TMP is U_FMT_filter_base ; :: thesis: verum

end;( not U_FMT x is empty & U_FMT x is with_non-empty_elements & ( for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2 ) )

proof

then
for x being Element of the carrier of TMP holds
let x be Element of the carrier of TMP; :: thesis: ( not U_FMT x is empty & U_FMT x is with_non-empty_elements & ( for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2 ) )

thus A8: not U_FMT x is empty by A6; :: thesis: ( U_FMT x is with_non-empty_elements & ( for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2 ) )

thus U_FMT x is with_non-empty_elements :: thesis: for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2

end;thus A8: not U_FMT x is empty by A6; :: thesis: ( U_FMT x is with_non-empty_elements & ( for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2 ) )

thus U_FMT x is with_non-empty_elements :: thesis: for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2

proof

thus
for B1, B2 being Element of U_FMT x ex B being Element of U_FMT x st B c= B1 /\ B2
:: thesis: verum
assume A9:
not U_FMT x is with_non-empty_elements
; :: thesis: contradiction

{} in H_{1}(x)
by A9, A5;

then consider O being Element of the topology of T such that

A10: O = {} and

A11: x in O ;

thus contradiction by A10, A11; :: thesis: verum

end;{} in H

then consider O being Element of the topology of T such that

A10: O = {} and

A11: x in O ;

thus contradiction by A10, A11; :: thesis: verum

proof

let B1, B2 be Element of U_FMT x; :: thesis: ex B being Element of U_FMT x st B c= B1 /\ B2

( B1 in U_FMT x & B2 in U_FMT x ) by A8;

then A12: ( B1 in H_{1}(x) & B2 in H_{1}(x) )
by A5;

then consider O1 being Element of the topology of T such that

A13: B1 = O1 and

A14: x in O1 ;

consider O2 being Element of the topology of T such that

A15: B2 = O2 and

A16: x in O2 by A12;

A17: x in O1 /\ O2 by A14, A16, XBOOLE_0:def 4;

reconsider OO = O1 /\ O2 as Element of the topology of T by PRE_TOPC:def 1;

OO in H_{1}(x)
by A17;

then reconsider OO = OO as Element of U_FMT x by A5;

take OO ; :: thesis: OO c= B1 /\ B2

thus OO c= B1 /\ B2 by A13, A15; :: thesis: verum

end;( B1 in U_FMT x & B2 in U_FMT x ) by A8;

then A12: ( B1 in H

then consider O1 being Element of the topology of T such that

A13: B1 = O1 and

A14: x in O1 ;

consider O2 being Element of the topology of T such that

A15: B2 = O2 and

A16: x in O2 by A12;

A17: x in O1 /\ O2 by A14, A16, XBOOLE_0:def 4;

reconsider OO = O1 /\ O2 as Element of the topology of T by PRE_TOPC:def 1;

OO in H

then reconsider OO = OO as Element of U_FMT x by A5;

take OO ; :: thesis: OO c= B1 /\ B2

thus OO c= B1 /\ B2 by A13, A15; :: thesis: verum

( not U_FMT x is empty & U_FMT x is with_non-empty_elements & U_FMT x is quasi_basis ) ;

hence TMP is U_FMT_filter_base ; :: thesis: verum

take ET ; :: thesis: ( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

thus ET is U_FMT_filter by A7, Th8; :: thesis: ( ET is U_FMT_with_point & ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

thus A18: ET is U_FMT_with_point :: thesis: ( ET is U_FMT_local & the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) )

proof

thus A26:
ET is U_FMT_local
:: thesis: ( the carrier of T = the carrier of ET & ex TT being FMT_TopSpace st
for x being Element of ET

for V being Element of U_FMT x holds x in V

end;for V being Element of U_FMT x holds x in V

proof

hence
ET is U_FMT_with_point
; :: thesis: verum
let x be Element of ET; :: thesis: for V being Element of U_FMT x holds x in V

let V be Element of U_FMT x; :: thesis: x in V

set Z = the BNbd of (gen_filter TMP) . x;

reconsider x0 = x as Element of TMP ;

A20: U_FMT x = <.(U_FMT x0).] by Def7;

A21: U_FMT x0 = H_{1}(x0)
by A5;

then reconsider FX0 = H_{1}(x0) as Subset-Family of the carrier of TMP ;

A22: V is Element of <.FX0.] by A5, A20;

not <.FX0.] is empty

then consider b being Element of FX0 such that

A23: b c= V by CARDFIL2:def 8;

not H_{1}(x0) is empty
_{1}(x0)
;

then consider OO being Element of the topology of T such that

A24: b = OO and

A25: x0 in OO ;

thus x in V by A23, A24, A25; :: thesis: verum

end;let V be Element of U_FMT x; :: thesis: x in V

set Z = the BNbd of (gen_filter TMP) . x;

reconsider x0 = x as Element of TMP ;

A20: U_FMT x = <.(U_FMT x0).] by Def7;

A21: U_FMT x0 = H

then reconsider FX0 = H

A22: V is Element of <.FX0.] by A5, A20;

not <.FX0.] is empty

proof

then
V in <.FX0.]
by A22;
the carrier of T in the topology of T
by PRE_TOPC:def 1;

then the carrier of T in FX0 ;

then reconsider XX = the carrier of T as Element of FX0 ;

FX0 c= <.FX0.] by CARDFIL2:def 8;

hence not <.FX0.] is empty by A21, A6; :: thesis: verum

end;then the carrier of T in FX0 ;

then reconsider XX = the carrier of T as Element of FX0 ;

FX0 c= <.FX0.] by CARDFIL2:def 8;

hence not <.FX0.] is empty by A21, A6; :: thesis: verum

then consider b being Element of FX0 such that

A23: b c= V by CARDFIL2:def 8;

not H

proof

then
b in H
the carrier of T in the topology of T
by PRE_TOPC:def 1;

then the carrier of T in H_{1}(x0)
;

hence not H_{1}(x0) is empty
; :: thesis: verum

end;then the carrier of T in H

hence not H

then consider OO being Element of the topology of T such that

A24: b = OO and

A25: x0 in OO ;

thus x in V by A23, A24, A25; :: thesis: verum

( TT = ET & Family_open_set TT = the topology of T ) )

proof

thus
the carrier of T = the carrier of ET
; :: thesis: ex TT being FMT_TopSpace st
for x being Element of ET

for V being Element of U_FMT x ex W being Element of U_FMT x st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

end;for V being Element of U_FMT x ex W being Element of U_FMT x st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

proof

hence
ET is U_FMT_local
; :: thesis: verum
let t be Element of ET; :: thesis: for V being Element of U_FMT t ex W being Element of U_FMT t st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

set Z = the BNbd of (gen_filter TMP) . t;

reconsider t0 = t as Element of TMP ;

A28: U_FMT t = <.(U_FMT t0).] by Def7;

A29: U_FMT t0 = H_{1}(t0)
by A5;

then reconsider FT0 = H_{1}(t0) as Subset-Family of the carrier of TMP ;

for V being Element of U_FMT t ex W being Element of U_FMT t st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y ; :: thesis: verum

end;for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

set Z = the BNbd of (gen_filter TMP) . t;

reconsider t0 = t as Element of TMP ;

A28: U_FMT t = <.(U_FMT t0).] by Def7;

A29: U_FMT t0 = H

then reconsider FT0 = H

for V being Element of U_FMT t ex W being Element of U_FMT t st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

proof

hence
for V being Element of U_FMT t ex W being Element of U_FMT t st
let V be Element of U_FMT t; :: thesis: ex W being Element of U_FMT t st

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

A30: not <.FT0.] is empty

consider V0 being Element of FT0 such that

A32: V0 c= V by A31, CARDFIL2:def 8;

A33: not H_{1}(t0) is empty
_{1}(t0)
;

then consider OUV being Element of the topology of T such that

A34: V0 = OUV and

A35: t0 in OUV ;

reconsider W = OUV as Element of U_FMT t by A28, A29, A34, CARDFIL2:def 8;

take W ; :: thesis: for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

V is Element of U_FMT y ; :: thesis: verum

end;for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

A30: not <.FT0.] is empty

proof

A31:
V in <.FT0.]
by A30, A28, A29;
the carrier of T in the topology of T
by PRE_TOPC:def 1;

then the carrier of T in FT0 ;

then reconsider XX = the carrier of T as Element of FT0 ;

XX in <.FT0.]

end;then the carrier of T in FT0 ;

then reconsider XX = the carrier of T as Element of FT0 ;

XX in <.FT0.]

proof end;

hence
not <.FT0.] is empty
; :: thesis: verumconsider V0 being Element of FT0 such that

A32: V0 c= V by A31, CARDFIL2:def 8;

A33: not H

proof

then
V0 in H
the carrier of T in the topology of T
by PRE_TOPC:def 1;

then the carrier of T in H_{1}(t0)
;

hence not H_{1}(t0) is empty
; :: thesis: verum

end;then the carrier of T in H

hence not H

then consider OUV being Element of the topology of T such that

A34: V0 = OUV and

A35: t0 in OUV ;

reconsider W = OUV as Element of U_FMT t by A28, A29, A34, CARDFIL2:def 8;

take W ; :: thesis: for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y

proof

hence
for y being Element of ET st y is Element of W holds
let y be Element of ET; :: thesis: ( y is Element of W implies V is Element of U_FMT y )

assume A36: y is Element of W ; :: thesis: V is Element of U_FMT y

set Z = the BNbd of (gen_filter TMP) . y;

reconsider y0 = y as Element of TMP ;

A38: U_FMT y0 = H_{1}(y0)
by A5;

then reconsider FY0 = H_{1}(y0) as Subset-Family of the carrier of TMP ;

A39: V0 in H_{1}(y0)
by A34, A36, A35;

( V0 in FT0 & FT0 c= bool the carrier of TMP ) by A33;

then reconsider VV0 = V0 as Subset of the carrier of TMP ;

V in <.FY0.] by A39, A32, A31, CARDFIL2:def 8;

hence V is Element of U_FMT y by Def7, A38; :: thesis: verum

end;assume A36: y is Element of W ; :: thesis: V is Element of U_FMT y

set Z = the BNbd of (gen_filter TMP) . y;

reconsider y0 = y as Element of TMP ;

A38: U_FMT y0 = H

then reconsider FY0 = H

A39: V0 in H

( V0 in FT0 & FT0 c= bool the carrier of TMP ) by A33;

then reconsider VV0 = V0 as Subset of the carrier of TMP ;

V in <.FY0.] by A39, A32, A31, CARDFIL2:def 8;

hence V is Element of U_FMT y by Def7, A38; :: thesis: verum

V is Element of U_FMT y ; :: thesis: verum

for y being Element of ET st y is Element of W holds

V is Element of U_FMT y ; :: thesis: verum

( TT = ET & Family_open_set TT = the topology of T )

ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T )

proof

hence
ex TT being FMT_TopSpace st
reconsider TT = ET as FMT_TopSpace by A7, Th8, A18, A26;

Family_open_set TT = the topology of T

( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum

end;Family_open_set TT = the topology of T

proof

hence
ex TT being FMT_TopSpace st
A41:
Family_open_set TT c= the topology of T

end;proof

the topology of T c= Family_open_set TT
for t being object st t in Family_open_set TT holds

t in the topology of T

end;t in the topology of T

proof

hence
Family_open_set TT c= the topology of T
; :: thesis: verum
let t be object ; :: thesis: ( t in Family_open_set TT implies t in the topology of T )

assume t in Family_open_set TT ; :: thesis: t in the topology of T

then consider O being open Subset of TT such that

A42: t = O ;

end;assume t in Family_open_set TT ; :: thesis: t in the topology of T

then consider O being open Subset of TT such that

A42: t = O ;

per cases
( O is empty or not O is empty )
;

end;

suppose
not O is empty
; :: thesis: t in the topology of T

reconsider O = O as Subset of T ;

A44: for x being Point of T st x in O holds

ex b being Subset of T st

( b is a_neighborhood of x & b c= O )

end;A44: for x being Point of T st x in O holds

ex b being Subset of T st

( b is a_neighborhood of x & b c= O )

proof

thus
t in the topology of T
by A44, CONNSP_2:7, A42, PRE_TOPC:def 2; :: thesis: verum
let x be Point of T; :: thesis: ( x in O implies ex b being Subset of T st

( b is a_neighborhood of x & b c= O ) )

assume A45: x in O ; :: thesis: ex b being Subset of T st

( b is a_neighborhood of x & b c= O )

reconsider x0 = x as Element of ET ;

A46: O in U_FMT x0 by A45, Def1;

set Z = the BNbd of (gen_filter TMP) . x0;

reconsider x1 = x0 as Element of TMP ;

O in <.(U_FMT x1).] by A46, Def7;

then consider b being Element of U_FMT x1 such that

A48: b c= O by CARDFIL2:def 8;

( not U_FMT x1 is empty & b is Element of U_FMT x1 ) by A6;

then b in U_FMT x1 ;

then b in H_{1}(x1)
by A5;

then consider b0 being Element of the topology of T such that

A49: b = b0 and

A50: x1 in b0 ;

b0 is open ;

hence ex b being Subset of T st

( b is a_neighborhood of x & b c= O ) by A48, A49, A50, CONNSP_2:3; :: thesis: verum

end;( b is a_neighborhood of x & b c= O ) )

assume A45: x in O ; :: thesis: ex b being Subset of T st

( b is a_neighborhood of x & b c= O )

reconsider x0 = x as Element of ET ;

A46: O in U_FMT x0 by A45, Def1;

set Z = the BNbd of (gen_filter TMP) . x0;

reconsider x1 = x0 as Element of TMP ;

O in <.(U_FMT x1).] by A46, Def7;

then consider b being Element of U_FMT x1 such that

A48: b c= O by CARDFIL2:def 8;

( not U_FMT x1 is empty & b is Element of U_FMT x1 ) by A6;

then b in U_FMT x1 ;

then b in H

then consider b0 being Element of the topology of T such that

A49: b = b0 and

A50: x1 in b0 ;

b0 is open ;

hence ex b being Subset of T st

( b is a_neighborhood of x & b c= O ) by A48, A49, A50, CONNSP_2:3; :: thesis: verum

proof

hence
Family_open_set TT = the topology of T
by A41; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in the topology of T or t in Family_open_set TT )

assume A51: t in the topology of T ; :: thesis: t in Family_open_set TT

then reconsider t = t as Subset of TT ;

t is open

end;assume A51: t in the topology of T ; :: thesis: t in Family_open_set TT

then reconsider t = t as Subset of TT ;

t is open

proof

hence
t in Family_open_set TT
; :: thesis: verum
for x being Element of ET st x in t holds

t in U_FMT x

end;t in U_FMT x

proof

hence
t is open
; :: thesis: verum
let x be Element of ET; :: thesis: ( x in t implies t in U_FMT x )

assume A53: x in t ; :: thesis: t in U_FMT x

set Z = the BNbd of (gen_filter TMP) . x;

reconsider x0 = x as Element of TMP ;

A55: U_FMT x = <.(U_FMT x0).] by Def7;

U_FMT x0 = H_{1}(x0)
by A5;

then reconsider FX0 = H_{1}(x0) as Subset-Family of the carrier of TMP ;

t in H_{1}(x0)
by A51, A53;

then t in U_FMT x0 by A5;

hence t in U_FMT x by A55, CARDFIL2:def 8; :: thesis: verum

end;assume A53: x in t ; :: thesis: t in U_FMT x

set Z = the BNbd of (gen_filter TMP) . x;

reconsider x0 = x as Element of TMP ;

A55: U_FMT x = <.(U_FMT x0).] by Def7;

U_FMT x0 = H

then reconsider FX0 = H

t in H

then t in U_FMT x0 by A5;

hence t in U_FMT x by A55, CARDFIL2:def 8; :: thesis: verum

( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum

( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum

A56: the carrier of T = the carrier of ET and

( ET is U_FMT_filter & ET is U_FMT_with_point & ET is U_FMT_local ) and

A57: ex TT being FMT_TopSpace st

( TT = ET & Family_open_set TT = the topology of T ) ;

consider TT being FMT_TopSpace such that

A58: TT = ET and

Family_open_set TT = the topology of T by A57;

take TT ; :: thesis: ( the carrier of T = the carrier of TT & Family_open_set TT = the topology of T )

thus ( the carrier of T = the carrier of TT & Family_open_set TT = the topology of T ) by A56, A57, A58; :: thesis: verum