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

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