let T be non empty TopSpace; :: thesis: for s being Function of , the carrier of T
for x being Point of T
for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B )

let s be Function of , the carrier of T; :: thesis: for x being Point of T
for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B )

let x be Point of T; :: thesis: for cB being basis of () holds
( x in lim_filter (s,) iff for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B )

let cB be basis of (); :: thesis: ( x in lim_filter (s,) iff for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B )

hereby :: thesis: ( ( for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B ) implies x in lim_filter (s,) )
assume A1: x in lim_filter (s,) ; :: thesis: for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B

hereby :: thesis: verum
let B be Element of cB; :: thesis: ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B

consider i, j being Nat such that
A2: s .: ( \ [:(Segm i),(Segm j):]) c= B by ;
take i = i; :: thesis: ex j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B

take j = j; :: thesis: for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B

thus for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B :: thesis: verum
proof
let m, n be Nat; :: thesis: ( ( i <= m or j <= n ) implies s . (m,n) in B )
assume A3: ( i <= m or j <= n ) ; :: thesis: s . (m,n) in B
( m in NAT & n in NAT ) by ORDINAL1:def 12;
then A4: [m,n] in by ZFMISC_1:def 2;
A5: ( not m in Segm i or not n in Segm j ) by ;
not [m,n] in [:(Segm i),(Segm j):]
proof
assume [m,n] in [:(Segm i),(Segm j):] ; :: thesis: contradiction
then ex a, b being object st
( a in Segm i & b in Segm j & [m,n] = [a,b] ) by ZFMISC_1:def 2;
hence contradiction by A5, XTUPLE_0:1; :: thesis: verum
end;
then A6: [m,n] in \ [:(Segm i),(Segm j):] by ;
[m,n] in dom s by ;
then s . [m,n] in s .: ( \ [:(Segm i),(Segm j):]) by ;
then s . [m,n] in B by A2;
hence s . (m,n) in B by BINOP_1:def 1; :: thesis: verum
end;
end;
end;
assume A7: for B being Element of cB ex i, j being Nat st
for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B ; :: thesis: x in lim_filter (s,)
now :: thesis: for B being Element of cB ex n1, n2 being Nat st s .: ( \ [:(Segm n1),(Segm n2):]) c= B
let B be Element of cB; :: thesis: ex n1, n2 being Nat st s .: ( \ [:(Segm n1),(Segm n2):]) c= B
consider i, j being Nat such that
A8: for m, n being Nat st ( i <= m or j <= n ) holds
s . (m,n) in B by A7;
s .: ( \ [:(Segm i),(Segm j):]) c= B
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in s .: ( \ [:(Segm i),(Segm j):]) or t in B )
assume t in s .: ( \ [:(Segm i),(Segm j):]) ; :: thesis: t in B
then consider a being object such that
A9: a in dom s and
A10: a in \ [:(Segm i),(Segm j):] and
A11: t = s . a by FUNCT_1:def 6;
reconsider a = a as Element of by A9;
consider a1, a2 being object such that
A12: a1 in NAT and
A13: a2 in NAT and
A14: a = [a1,a2] by ZFMISC_1:def 2;
reconsider a1 = a1, a2 = a2 as Nat by ;
( not a1 in Segm i or not a2 in Segm j )
proof
assume ( a1 in Segm i & a2 in Segm j ) ; :: thesis: contradiction
then [a1,a2] in [:(Segm i),(Segm j):] by ZFMISC_1:def 2;
hence contradiction by A14, A10, XBOOLE_0:def 5; :: thesis: verum
end;
then A15: ( i <= a1 or j <= a2 ) by NAT_1:44;
t = s . (a1,a2) by ;
hence t in B by ; :: thesis: verum
end;
hence ex n1, n2 being Nat st s .: ( \ [:(Segm n1),(Segm n2):]) c= B ; :: thesis: verum
end;
hence x in lim_filter (s,) by Th52; :: thesis: verum