let T be non empty TopSpace; :: thesis: for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )
let s be sequence of the carrier of T; :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )
let x be Point of T; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )

hereby :: thesis: ( ( for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b ) implies x in lim_f s )

assume A1: x in lim_f s ; :: thesis: for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b

now :: thesis: for b being Element of B ex i1 being Nat st
for k being Nat st i1 <= k holds
s . k in b

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

now :: thesis: for k being Nat st i1 <= k holds
s . k in b

let k be Nat; :: thesis: ( i1 <= k implies s . k in b )
assume A3: i1 <= k ; :: thesis: s . k in b
reconsider k0 = k as Element of NAT by ORDINAL1:def 12;
i0 <= k0 by A3;
hence s . k in b by A2; :: thesis: verum

end;

hence for k being Nat st i1 <= k holds
s . k in b ; :: thesis: verum

end;

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

end;

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

now :: thesis: for b being Element of B ex i1 being Element of NAT st
for j being Element of NAT st i1 <= j holds
s . j in b

let b be Element of B; :: thesis: ex i1 being Element of NAT st
for j being Element of NAT st i1 <= j holds
s . j in b
consider i0 being Nat such that
A5: for j being Nat st i0 <= j holds
s . j in b by A4;
reconsider i1 = i0 as Element of NAT by ORDINAL1:def 12;
take i1 = i1; :: thesis: for j being Element of NAT st i1 <= j holds
s . j in b
thus for j being Element of NAT st i1 <= j holds
s . j in b by A5; :: thesis: verum

end;

hence x in lim_f s by Th45; :: thesis: verum