set X = {{}};
set f = {{}} --> {{{}}};
A1: {{{{}}}} c= bool (bool {{}})

proof

{{{}}} c= bool {{}}

proof

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;

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

end;

A3: ( dom ({{}} --> {{{}}}) = {{}} & rng ({{}} --> {{{}}}) = {{{{}}}} ) by RELAT_1:160;
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

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;

( FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter )

proof

A5: now :: thesis: for x being Element 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;

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

proof

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;

for x being Element of FMT
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

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;

hence ( FMT is U_FMT_local & FMT is U_FMT_with_point & FMT is U_FMT_filter ) by A5, A6; :: thesis: verum

end;

hence ex b₁ being non empty strict FMT_Space_Str st
( b₁ is U_FMT_local & b₁ is U_FMT_with_point & b₁ is U_FMT_filter ) ; :: thesis: verum