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 holds sequence_to_net s is_eventually_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 holds sequence_to_net s is_eventually_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 holds sequence_to_net s is_eventually_in b )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_f s iff for b being Element of B holds sequence_to_net s is_eventually_in b )

hereby :: thesis: ( ( for b being Element of B holds sequence_to_net s is_eventually_in b ) implies x in lim_f s )

assume x in lim_f s ; :: thesis: for b being Element of B holds sequence_to_net s is_eventually_in b
then for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b by Th42;
hence for b being Element of B holds sequence_to_net s is_eventually_in b by Th44; :: thesis: verum

end;

assume for b being Element of B holds sequence_to_net s is_eventually_in b ; :: thesis: x in lim_f s
then for b being Element of B ex i being Element of (sequence_to_net s) st
for j being Element of (sequence_to_net s) st i <= j holds
(sequence_to_net s) . j in b by Th43;
then for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b by Th44;
hence x in lim_f s by Th42; :: thesis: verum