:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :
for R being non empty RelStr
for N being prenet of R
for b₃ being strict prenet of R holds
( b₃ = inf_net N iff ex f being Function of N,R st
( b₃ = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) );