let x, y be set ; 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; ( [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
; 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; verum