:: deftheorem defines lim_inf WAYBEL11:def 6 :
for R being non empty RelStr
for N being net of R holds lim_inf N = "\/" ( { ("/\" ( { (N . i) where i is Element of N : i >= j } ,R)) where j is Element of N : verum } ,R);