let x, y be set ; :: thesis: for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds
y in the carrier of N
let N be Pnet; :: thesis: ( [x,y] in Flow N & x in the carrier' of N implies y in the carrier of N )
assume that
A1: [x,y] in Flow N and
A2: x in the carrier' of N ; :: thesis: y in the carrier of N
A3: not x in the carrier of N by A2, Th11;
Flow N c= [:the carrier of N,the carrier' of N:] \/ [:the carrier' of N,the carrier of N:] by Def1;
then ( [x,y] in [:the carrier of N,the carrier' of N:] or [x,y] in [:the carrier' of N,the carrier of N:] ) by A1, XBOOLE_0:def 3;
hence y in the carrier of N by A3, ZFMISC_1:106; :: thesis: verum