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 n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) 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 n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) 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 n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )

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

( ( for B being Element of cB ex n being Nat st s .: () c= B ) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
proof
hereby :: thesis: ( ( for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B ) implies for B being Element of cB ex n being Nat st s .: () c= B )
assume A1: for B being Element of cB ex n being Nat st s .: () c= B ; :: thesis: for B being Element of cB ex n0 being Nat st
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B

hereby :: thesis: verum
let B be Element of cB; :: thesis: ex n0 being Nat st
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B

consider n0 being Nat such that
A2: s .: () c= B by A1;
take n0 = n0; :: thesis: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B

thus for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B by ; :: thesis: verum
end;
end;
assume A3: for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B ; :: thesis: for B being Element of cB ex n being Nat st s .: () c= B
hereby :: thesis: verum
let B be Element of cB; :: thesis: ex n being Nat st s .: () c= B
consider n0 being Nat such that
A4: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B by A3;
thus ex n being Nat st s .: () c= B :: thesis: verum
proof
take n0 ; :: thesis: s .: () c= B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in s .: () or x in B )
assume x in s .: () ; :: thesis: x in B
then ex n1, n2 being Nat st
( n0 <= n1 & n0 <= n2 & x = s . (n1,n2) ) by Th53;
hence x in B by A4; :: thesis: verum
end;
end;
end;
hence ( x in lim_filter (s,) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B ) by Th50; :: thesis: verum