let x be Point of FMT_R^1; :: thesis: for z being Point of (TopSpaceMetr RealSpace)
for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds
<.SF.] = U_FMT x
let z be Point of (TopSpaceMetr RealSpace); :: thesis: for SF being Subset-Family of FMT_R^1 st x = z & SF = Balls z holds
<.SF.] = U_FMT x
let SF be Subset-Family of FMT_R^1; :: thesis: ( x = z & SF = Balls z implies <.SF.] = U_FMT x )
assume that
A1: x = z and
A2: SF = Balls z ; :: thesis: <.SF.] = U_FMT x
consider zy being Point of RealSpace such that
A3: z = zy and
A4: Balls z = { (Ball (zy,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
now :: thesis: ( { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } c= U_FMT x & U_FMT x c= { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } )
now :: thesis: for a being object st a in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } holds
a in U_FMT x
let a be object ; :: thesis: ( a in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } implies a in U_FMT x )
assume a in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } ; :: thesis: a in U_FMT x
then consider y being Subset of FMT_R^1 such that
A5: a = y and
A6: ex b being Element of SF st b c= y ;
consider b being Element of SF such that
A7: b c= y by A6;
b in Balls z by A2;
then consider n being Nat such that
A8: b = Ball (zy,(1 / n)) and
A9: n <> 0 by A4;
reconsider r = 1 / n as Real ;
now :: thesis: ( 0 / n < 1 / n & 0 / n = 0 )
now :: thesis: ( 0 < n & 0 < 1 )
( 0 <= n & n <> 0 ) by A9, NAT_1:2;
hence 0 < n by XXREAL_0:1; :: thesis: 0 < 1
thus 0 < 1 ; :: thesis: verum
end;
hence 0 / n < 1 / n by XREAL_1:74; :: thesis: 0 / n = 0
thus 0 / n = 0 ; :: thesis: verum
end;
then b is a_neighborhood of x by A1, A8, A3, Th61;
then b in U_FMT x by FINTOPO7:def 5;
hence a in U_FMT x by A5, A7, CARD_FIL:def 1; :: thesis: verum
end;
hence { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } c= U_FMT x ; :: thesis: U_FMT x c= { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x }
now :: thesis: for o being object st o in U_FMT x holds
o in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x }
let o be object ; :: thesis: ( o in U_FMT x implies o in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } )
assume A10: o in U_FMT x ; :: thesis: o in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x }
then reconsider o9 = o as Subset of FMT_R^1 ;
reconsider Io9 = Int o9 as open a_neighborhood of x by A10, FINTOPO7:def 5, Th14;
Io9 in U_FMT x by FINTOPO7:def 5;
then consider r being Real such that
A11: r > 0 and
A12: ].(x - r),(x + r).[ c= Io9 by FINTOPO7:def 3, Th55;
consider n being Nat such that
A13: 1 / n < r and
A14: n > 0 by A11, FRECHET:36;
A15: ].(x - (1 / n)),(x + (1 / n)).[ c= ].(x - r),(x + r).[ by A13, INTEGRA6:2;
reconsider n1 = 1 / n as Real ;
].(x - (1 / n)),(x + (1 / n)).[ = Ball (zy,(1 / n)) by A1, A3, FRECHET:7;
then ].(x - (1 / n)),(x + (1 / n)).[ in { (Ball (zy,(1 / n))) where n is Nat : n <> 0 } by A14;
then reconsider b = ].(x - (1 / n)),(x + (1 / n)).[ as Element of SF by A2, A4;
( b c= Io9 & Io9 c= o9 ) by A12, A15, Lm15;
then b c= o9 ;
hence o in { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } ; :: thesis: verum
end;
hence U_FMT x c= { x where x is Subset of FMT_R^1 : ex b being Element of SF st b c= x } ; :: thesis: verum
end;
hence <.SF.] = U_FMT x by CARDFIL2:14; :: thesis: verum