:: deftheorem defines ex_inf_of WAYBEL_9:def 4 :
for L being RelStr
for N being NetStr over L holds
( ex_inf_of N iff ex_inf_of rng the mapping of N,L );