:: deftheorem defines is_S-limit_of WAYBEL11:def 7 :
for R being non empty reflexive RelStr
for N being net of R
for p being Element of R holds
( p is_S-limit_of N iff p <= lim_inf N );