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