for R being non empty transitive RelStr
for S being non empty set
for f being Function of S, the carrier of R st S c= the carrier of R & Net-Str (S,f) is directed holds
Net-Str (S,f) in NetUniv R