set X = ;
set f = --> ;
A1: {} c= 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:
then A2: x = by TARSKI:def 1;
{{}} c= ;
hence x in bool by A2; :: thesis: verum
end;
then {} in bool () ;
hence {} c= bool () by TARSKI:def 1; :: thesis: verum
end;
A3: ( dom () = & rng () = ) by RELAT_1:160;
reconsider f = --> as PartFunc of ,(bool ()) by ;
reconsider f = f as Function of ,(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:
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 ; :: 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 b1 being non empty strict FMT_Space_Str st
( b1 is U_FMT_local & b1 is U_FMT_with_point & b1 is U_FMT_filter ) ; :: thesis: verum