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, Th4;

Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2;

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:87; :: thesis: verum

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, Th4;

Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2;

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:87; :: thesis: verum