let T be non empty TopSpace; :: thesis:
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

deffunc H₁( 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₁(x) in bool (bool the carrier of T)

proof

let x be object ; :: thesis:
assume A2: x in the carrier of T ; :: thesis:
reconsider x = x as Element of T by A2;
H₁(x) c= bool the carrier of T

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: t in H₁(x) ; :: thesis:
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:

end;

hence H₁(x) in bool (bool the carrier of T) ; :: thesis:

end;

ex f being Function of the carrier of T,(bool (bool the carrier of T)) st
for x being object st x in the carrier of T holds
f . x = H₁(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₁(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

proof

let t be Element of TMP; :: thesis:
take TT = the carrier of T; :: according to XBOOLE_0:def 1 :: thesis:
TT in the topology of T by PRE_TOPC:def 1;
then TT in H₁(t) ;
hence TT in U_FMT t by A5; :: thesis:

end;

A7: TMP is U_FMT_filter_base

proof

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 ) )

proof

let x be Element of the carrier of TMP; :: thesis:
thus A8: not U_FMT x is empty by A6; :: thesis:
thus U_FMT x is with_non-empty_elements :: thesis:

proof

assume A9: not U_FMT x is with_non-empty_elements ; :: thesis:
{} in H₁(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:

end;

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

proof

let B1, B2 be Element of U_FMT x; :: thesis:
( B1 in U_FMT x & B2 in U_FMT x ) by A8;
then A12: ( B1 in H₁(x) & B2 in H₁(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₁(x) by A17;
then reconsider OO = OO as Element of U_FMT x by A5;
take OO ; :: thesis:
thus OO c= B1 /\ B2 by A13, A15; :: thesis:

end;

then for x being Element of the carrier of TMP holds
( 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:

end;

reconsider ET = gen_filter TMP as non empty strict FMT_Space_Str ;
take ET ; :: thesis:
thus ET is U_FMT_filter by A7, Th8; :: thesis:
thus A18: ET is U_FMT_with_point :: thesis:

proof

for x being Element of ET
for V being Element of U_FMT x holds x in V

proof

let x be Element of ET; :: thesis:
let V be Element of U_FMT x; :: thesis:
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₁(x0) by A5;
then reconsider FX0 = H₁(x0) as Subset-Family of the carrier of TMP ;
A22: V is Element of <.FX0.] by A5, A20;
not <.FX0.] is empty

proof

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:

end;

then V in <.FX0.] by A22;
then consider b being Element of FX0 such that
A23: b c= V by CARDFIL2:def 8;
not H₁(x0) is empty

proof

the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in H₁(x0) ;
hence not H₁(x0) is empty ; :: thesis:

end;

then b in H₁(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:

end;

hence ET is U_FMT_with_point ; :: thesis:

end;

thus A26: ET is U_FMT_local :: thesis:

proof

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

proof

let t be Element of ET; :: thesis:
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₁(t0) by A5;
then reconsider FT0 = H₁(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

proof

let V be Element of U_FMT t; :: thesis:
A30: not <.FT0.] is empty

proof

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.]

proof

( XX is Element of FT0 & XX c= XX ) ;
hence XX in <.FT0.] by CARDFIL2:def 8; :: thesis:

end;

hence not <.FT0.] is empty ; :: thesis:

end;

A31: V in <.FT0.] by A30, A28, A29;
consider V0 being Element of FT0 such that
A32: V0 c= V by A31, CARDFIL2:def 8;
A33: not H₁(t0) is empty

proof

the carrier of T in the topology of T by PRE_TOPC:def 1;
then the carrier of T in H₁(t0) ;
hence not H₁(t0) is empty ; :: thesis:

end;

then V0 in H₁(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

proof

let y be Element of ET; :: thesis:
assume A36: y is Element of W ; :: thesis:
set Z = the BNbd of (gen_filter TMP) . y;
reconsider y0 = y as Element of TMP ;
A38: U_FMT y0 = H₁(y0) by A5;
then reconsider FY0 = H₁(y0) as Subset-Family of the carrier of TMP ;
A39: V0 in H₁(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:

end;

hence for y being Element of ET st y is Element of W holds
V is Element of U_FMT y ; :: thesis:

end;

hence 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 ; :: thesis:

end;

hence ET is U_FMT_local ; :: thesis:

end;

thus the carrier of T = the carrier of ET ; :: thesis:
ex TT being FMT_TopSpace st
( TT = ET & Family_open_set TT = the topology of T )

proof

reconsider TT = ET as FMT_TopSpace by A7, Th8, A18, A26;
Family_open_set TT = the topology of T

proof

A41: Family_open_set TT c= the topology of T

proof

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

proof

let t be object ; :: thesis:
assume t in Family_open_set TT ; :: thesis:
then consider O being open Subset of TT such that
A42: t = O ;

per cases ;

suppose O is empty ; :: thesis:

hence t in the topology of T by A42, PRE_TOPC:1; :: thesis:

end;

suppose not O is empty ; :: thesis:

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 )

proof

let x be Point of T; :: thesis:
assume A45: x in O ; :: thesis:
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₁(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:

end;

thus t in the topology of T by A44, CONNSP_2:7, A42, PRE_TOPC:def 2; :: thesis:

end;

hence Family_open_set TT c= the topology of T ; :: thesis:

end;

the topology of T c= Family_open_set TT

proof

let t be object ; :: according to TARSKI:def 3 :: thesis:
assume A51: t in the topology of T ; :: thesis:
then reconsider t = t as Subset of TT ;
t is open

proof

for x being Element of ET st x in t holds
t in U_FMT x

proof

let x be Element of ET; :: thesis:
assume A53: x in t ; :: thesis:
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₁(x0) by A5;
then reconsider FX0 = H₁(x0) as Subset-Family of the carrier of TMP ;
t in H₁(x0) by A51, A53;
then t in U_FMT x0 by A5;
hence t in U_FMT x by A55, CARDFIL2:def 8; :: thesis:

end;

hence t is open ; :: thesis:

end;

hence t in Family_open_set TT ; :: thesis:

end;

hence Family_open_set TT = the topology of T by A41; :: thesis:

end;

hence ex TT being FMT_TopSpace st
( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis:

end;

hence ex TT being FMT_TopSpace st
( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis:

end;

then consider ET being non empty strict FMT_Space_Str such that
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:
thus ( the carrier of T = the carrier of TT & Family_open_set TT = the topology of T ) by A56, A57, A58; :: thesis: