:: deftheorem defines inf WAYBEL_9:def 2 :
for L being non empty RelStr
for N being NetStr over L holds inf N = Inf ;