theorem :: NET_1:7

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