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 ) )
proof
deffunc H1( 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
H1(x) in bool (bool the carrier of T)
proof
let x be object ; :: thesis: ( x in the carrier of T implies H1(x) in bool (bool the carrier of T) )
assume A2: x in the carrier of T ; :: thesis: H1(x) in bool (bool the carrier of T)
reconsider x = x as Element of T by A2;
H1(x) c= bool the carrier of T
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in H1(x) or t in bool the carrier of T )
assume A3: t in H1(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;
hence H1(x) in bool (bool the carrier of T) ; :: thesis: verum
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 = H1(x) from 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 = H1(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: 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 H1(t) ;
hence TT in U_FMT t by A5; :: thesis: verum
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: ( 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
proof
assume A9: not U_FMT x is with_non-empty_elements ; :: thesis: contradiction
{} in H1(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;
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
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 H1(x) & B2 in H1(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 ;
reconsider OO = O1 /\ O2 as Element of the topology of T by PRE_TOPC:def 1;
OO in H1(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 ; :: thesis: verum
end;
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: verum
end;
reconsider ET = gen_filter TMP as non empty strict FMT_Space_Str ;
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 ; :: 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
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: 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 = H1(x0) by A5;
then reconsider FX0 = H1(x0) as Subset-Family of the carrier of TMP ;
A22: V is Element of <.FX0.] by ;
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 ; :: thesis: verum
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 H1(x0) is empty then b in H1(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 ; :: thesis: verum
end;
hence ET is U_FMT_with_point ; :: thesis: verum
end;
thus A26: ET is U_FMT_local :: thesis: ( 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
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: 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 = H1(t0) by A5;
then reconsider FT0 = H1(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: 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
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: verum
end;
hence not <.FT0.] is empty ; :: thesis: verum
end;
A31: V in <.FT0.] by ;
consider V0 being Element of FT0 such that
A32: V0 c= V by ;
A33: not H1(t0) is empty then V0 in H1(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 ;
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
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 = H1(y0) by A5;
then reconsider FY0 = H1(y0) as Subset-Family of the carrier of TMP ;
A39: V0 in H1(y0) by ;
( 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 ;
hence V is Element of U_FMT y by ; :: thesis: verum
end;
hence for y being Element of ET st y is Element of W holds
V is Element of U_FMT y ; :: thesis: verum
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: verum
end;
hence ET is U_FMT_local ; :: thesis: verum
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 )

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: ( 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 ;
per cases ( O is empty or not O is empty ) ;
suppose O is empty ; :: thesis: t in the topology of T
hence t in the topology of T by ; :: thesis: verum
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 )
proof
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 ;
set Z = the BNbd of (gen_filter TMP) . x0;
reconsider x1 = x0 as Element of TMP ;
O in <.(U_FMT x1).] by ;
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 H1(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 ; :: thesis: verum
end;
thus t in the topology of T by ; :: thesis: verum
end;
end;
end;
hence Family_open_set TT c= the topology of T ; :: thesis: verum
end;
the topology of T c= Family_open_set TT
proof
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:
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: ( 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 = H1(x0) by A5;
then reconsider FX0 = H1(x0) as Subset-Family of the carrier of TMP ;
t in H1(x0) by ;
then t in U_FMT x0 by A5;
hence t in U_FMT x by ; :: thesis: verum
end;
hence t is open ; :: thesis: verum
end;
hence t in Family_open_set TT ; :: thesis: verum
end;
hence Family_open_set TT = the topology of T by A41; :: thesis: verum
end;
hence ex TT being FMT_TopSpace st
( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum
end;
hence ex TT being FMT_TopSpace st
( TT = ET & Family_open_set TT = the topology of T ) ; :: thesis: verum
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: ( 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 ; :: thesis: verum