theorem Th20: :: WAYBEL11:20

for R being non empty RelStr
for S being non empty set
for f being Function of S, the carrier of R st rng f is directed holds
Net-Str (S,f) is directed