let M be non empty MetrSpace; :: thesis: for L being non empty reflexive transitive RelStr

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let f be Function of ([#] L), the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let x be Point of (TopSpaceMetr M); :: thesis: ( [#] L is directed implies ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b ) )

assume A1: [#] L is directed ; :: thesis: ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;

hence ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b ) by A1, CARDFIL2:84; :: thesis: verum

for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let L be non empty reflexive transitive RelStr ; :: thesis: for f being Function of ([#] L), the carrier of (TopSpaceMetr M)

for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let f be Function of ([#] L), the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) st [#] L is directed holds

( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

let x be Point of (TopSpaceMetr M); :: thesis: ( [#] L is directed implies ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b ) )

assume A1: [#] L is directed ; :: thesis: ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b )

Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;

hence ( x in lim_f f iff for b being Element of Balls x ex n being Element of L st

for m being Element of L st n <= m holds

f . m in b ) by A1, CARDFIL2:84; :: thesis: verum