theorem Th28: :: WAYBEL11:28

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