assume lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) <> {} ; :: thesis: contradiction
then not lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) is empty ;
then consider x being object such that
A1: x in lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) ;
A2: lim_filter ((# dblseq_ex_1),(Frechet_Filter [:NAT,NAT:])) c= lim_filter ((# dblseq_ex_1),<.all-square-uparrow.)) by Th56;
A3: <.all-square-uparrow.) = <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by Th34, CARDFIL2:19, Th35;
then consider y being Real such that
A4: lim_filter ((# dblseq_ex_1),<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) = {y} by A1, A2, Th59;
y = 0 by A4, Th64;
then A5: x = 0 by A1, A2, A3, A4, TARSKI:def 1;
reconsider xp = 0 as Point of (TopSpaceMetr RealSpace) by Th64;
A6: Balls xp is basis of (BOOL2F (NeighborhoodSystem xp)) 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