theorem Th5: :: NET_1:5

for x, y being set
for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds
y in the carrier of N