assume lim_filter ((),) <> {} ; :: thesis: contradiction
then not lim_filter ((),) is empty ;
then consider x being object such that
A1: x in lim_filter ((),) ;
A2: lim_filter ((),) c= lim_filter ((),) by Th56;
A3: <.all-square-uparrow.) = by ;
then consider y being Real such that
A4: lim_filter ((),) = {y} by A1, A2, Th59;
y = 0 by ;
then A5: x = 0 by ;
reconsider xp = 0 as Point of by Th64;
A6: Balls xp is basis of () by CARDFIL3:6;
consider yr being Point of RealSpace such that
A7: yr = xp and
A8: Balls xp = { (Ball (yr,(1 / n))) where n is Nat : n <> 0 } by FRECHET:def 1;
Ball (yr,(1 / 2)) in Balls xp by A8;
then consider i, j being Nat such that
A9: for m, n being Nat st ( i <= m or j <= n ) holds
dblseq_ex_1 . (m,n) in Ball (yr,(1 / 2)) by A6, A5, A1, Th55;
dblseq_ex_1 . (0,j) in Ball (yr,(1 / 2)) by A9;
then dblseq_ex_1 . (0,j) in ].(yr - (1 / 2)),(yr + (1 / 2)).[ by FRECHET:7;
then 1 / (0 + 1) in ].(yr - (1 / 2)),(yr + (1 / 2)).[ by Def5;
hence contradiction by A7, XXREAL_1:4; :: thesis: verum