let T be non empty TopSpace; :: thesis: for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let f be Function of ([#] L), the carrier of T; :: thesis: for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let x be Point of T; :: thesis: for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
let B be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( [#] L is directed implies ( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ) )
assume A1: [#] L is directed ; :: thesis: ( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )

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

assume x in lim_f f ; :: thesis: for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b
then consider x0 being Element of T such that
A2: x = x0 and
A3: filter_image (f,(Tails_Filter L)) is_filter-finer_than NeighborhoodSystem x0 ;
BOOL2F (NeighborhoodSystem x) is_filter-coarser_than filter_image (f,(Tails_Filter L)) by A2, A3;
then A4: B is_coarser_than f .: (# (Tails L)) by A1, Th19;
reconsider B1 = B as filter_base of ([#] T) by Th09;
for b being Element of B1 ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b by A1, A4, Th20;
hence for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ; :: thesis: verum

end;

assume A5: for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b ; :: thesis: x in lim_f f
reconsider B1 = B as filter_base of ([#] T) by Th09;
for b being Element of B1 ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b by A5;
then B is_coarser_than f .: (# (Tails L)) by A1, Th20;
then BOOL2F (NeighborhoodSystem x) is_filter-coarser_than filter_image (f,(Tails_Filter L)) by A1, Th19;
then ( x is Element of T & filter_image (f,(Tails_Filter L)) is_filter-finer_than NeighborhoodSystem x ) ;
hence x in lim_f f ; :: thesis: verum