let x, y be set ; :: thesis: for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds
x in the carrier of N
let N be Pnet; :: thesis: ( [x,y] in Flow N & y in the carrier' of N implies x in the carrier of N )
assume that
A1: [x,y] in Flow N and
A2: y in the carrier' of N ; :: thesis: x in the carrier of N
A3: not y 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 x in the carrier of N by A3, ZFMISC_1:87; :: thesis: verum