let T be non empty TopSpace; :: thesis:
let s be sequence of the carrier of T; :: thesis:
let x be Point of T; :: thesis:
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis:

now :: thesis:

hereby :: thesis:

assume A1: x in lim_filter (s,(Frechet_Filter NAT)) ; :: thesis:

now :: thesis:

let b be Element of B; :: thesis:
consider i0 being Element of OrderedNAT such that
A2: for j being Element of OrderedNAT st i0 <= j holds
s . j in b by A1, Th41;
reconsider i1 = i0 as Element of NAT ;

now :: thesis:

let j be Element of NAT ; :: thesis:
assume A3: i1 <= j ; :: thesis:
reconsider j1 = j as Element of OrderedNAT ;
i0 <= j1 by A3;
hence s . j in b by A2; :: thesis:

end;

hence ex i being Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b ; :: thesis:

end;

hence for b being Element of B ex i being Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b ; :: thesis:

end;

assume A4: for b being Element of B ex i being Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b ; :: thesis:

now :: thesis:

let b be Element of B; :: thesis:
consider i0 being Element of NAT such that
A5: for j being Element of NAT st i0 <= j holds
s . j in b by A4;
reconsider i1 = i0 as Element of OrderedNAT ;

now :: thesis:

let j be Element of OrderedNAT; :: thesis:
assume A6: i1 <= j ; :: thesis:
consider x, y being Element of NAT such that
A7: [i1,j] = [x,y] and
A8: x <= y by A6;
( i1 = x & j = y & x <= y ) by A7, A8, XTUPLE_0:1;
hence s . j in b by A5; :: thesis:

end;

hence ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ; :: thesis:

end;

hence x in lim_filter (s,(Frechet_Filter NAT)) by Th41; :: thesis:

end;

hence ( x in lim_f s iff for b being Element of B ex i being Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b ) ; :: thesis: