set X = {{}};

set f = {{}} --> {{{}}};

A1: {{{{}}}} c= bool (bool {{}})

reconsider f = {{}} --> {{{}}} as PartFunc of {{}},(bool (bool {{}})) by A1, A3, FUNCT_2:2;

reconsider f = f as Function of {{}},(bool (bool {{}})) ;

reconsider FMT = FMT_Space_Str(# {{}},f #) as non empty strict FMT_Space_Str ;

A4: for x being Element of FMT holds U_FMT x = {{{}}}_{1} being non empty strict FMT_Space_Str st

( b_{1} is U_FMT_local & b_{1} is U_FMT_with_point & b_{1} is U_FMT_filter )
; :: thesis: verum

set f = {{}} --> {{{}}};

A1: {{{{}}}} c= bool (bool {{}})

proof

A3:
( dom ({{}} --> {{{}}}) = {{}} & rng ({{}} --> {{{}}}) = {{{{}}}} )
by RELAT_1:160;
{{{}}} c= bool {{}}

hence {{{{}}}} c= bool (bool {{}}) by TARSKI:def 1; :: thesis: verum

end;proof

then
{{{}}} in bool (bool {{}})
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {{{}}} or x in bool {{}} )

assume x in {{{}}} ; :: thesis: x in bool {{}}

then A2: x = {{}} by TARSKI:def 1;

{{}} c= {{}} ;

hence x in bool {{}} by A2; :: thesis: verum

end;assume x in {{{}}} ; :: thesis: x in bool {{}}

then A2: x = {{}} by TARSKI:def 1;

{{}} c= {{}} ;

hence x in bool {{}} by A2; :: thesis: verum

hence {{{{}}}} c= bool (bool {{}}) by TARSKI:def 1; :: thesis: verum

reconsider f = {{}} --> {{{}}} as PartFunc of {{}},(bool (bool {{}})) by A1, A3, FUNCT_2:2;

reconsider f = f as Function of {{}},(bool (bool {{}})) ;

reconsider FMT = FMT_Space_Str(# {{}},f #) as non empty strict FMT_Space_Str ;

A4: for x being Element of FMT holds U_FMT x = {{{}}}

proof

( FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter )
let x be Element of FMT; :: thesis: U_FMT x = {{{}}}

the BNbd of FMT . x in {{{{}}}} by FUNCT_2:5;

hence U_FMT x = {{{}}} by TARSKI:def 1; :: thesis: verum

end;the BNbd of FMT . x in {{{{}}}} by FUNCT_2:5;

hence U_FMT x = {{{}}} by TARSKI:def 1; :: thesis: verum

proof

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

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

V is Element of U_FMT y

end;

hence
ex bA5: now :: thesis: for x being Element of FMT

for V being Element of U_FMT x holds x in V

A6:
for x being Element of FMT holds U_FMT x is Filter of the carrier of FMT
for V being Element of U_FMT x holds x in V

let x be Element of FMT; :: 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

not U_FMT x is empty by A4;

then V in U_FMT x ;

then V in {{{}}} by A4;

then V = {{}} by TARSKI:def 1;

hence x in V ; :: thesis: verum

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

not U_FMT x is empty by A4;

then V in U_FMT x ;

then V in {{{}}} by A4;

then V = {{}} by TARSKI:def 1;

hence x in V ; :: thesis: verum

proof

for x being Element of FMT
let x be Element of FMT; :: thesis: U_FMT x is Filter of the carrier of FMT

reconsider Z = {{{}}} as Filter of {{}} by CARD_FIL:4;

( the carrier of FMT = {{}} & Z = {{{}}} & Z is Filter of {{}} ) ;

hence U_FMT x is Filter of the carrier of FMT by A4; :: thesis: verum

end;reconsider Z = {{{}}} as Filter of {{}} by CARD_FIL:4;

( the carrier of FMT = {{}} & Z = {{{}}} & Z is Filter of {{}} ) ;

hence U_FMT x is Filter of the carrier of FMT by A4; :: thesis: verum

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

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

V is Element of U_FMT y

proof

hence
( FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter )
by A5, A6; :: thesis: verum
let x be Element of FMT; :: thesis: for V being Element of U_FMT x ex W being Element of U_FMT x st

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

V is Element of U_FMT y

let V be Element of U_FMT x; :: thesis: ex W being Element of U_FMT x st

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

V is Element of U_FMT y

A7: V is Element of {{{}}} by A4;

take {{}} ; :: thesis: ( {{}} is Element of U_FMT x & ( for y being Element of FMT st y is Element of {{}} holds

V is Element of U_FMT y ) )

thus ( {{}} is Element of U_FMT x & ( for y being Element of FMT st y is Element of {{}} holds

V is Element of U_FMT y ) ) by A7, A4, TARSKI:def 1; :: thesis: verum

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

V is Element of U_FMT y

let V be Element of U_FMT x; :: thesis: ex W being Element of U_FMT x st

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

V is Element of U_FMT y

A7: V is Element of {{{}}} by A4;

take {{}} ; :: thesis: ( {{}} is Element of U_FMT x & ( for y being Element of FMT st y is Element of {{}} holds

V is Element of U_FMT y ) )

thus ( {{}} is Element of U_FMT x & ( for y being Element of FMT st y is Element of {{}} holds

V is Element of U_FMT y ) ) by A7, A4, TARSKI:def 1; :: thesis: verum

( b