for S being non empty reflexive antisymmetric RelStr
for e being Element of S holds e = lim_inf (Net-Str e)