let x, y be set ; :: thesis: for N being Pnet st [x,y] in the Flow of N & y in the Transitions of N holds
x in the Places of N
let N be Pnet; :: thesis: ( [x,y] in the Flow of N & y in the Transitions of N implies x in the Places of N )
assume A1: ( [x,y] in the Flow of N & y in the Transitions of N ) ; :: thesis: x in the Places of N
the Flow of N c= [:the Places of N,the Transitions of N:] \/ [:the Transitions of N,the Places of N:] by Def1;
then A2: ( [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;
not y in the Places of N by A1, Th11;
hence x in the Places of N by A2, ZFMISC_1:106; :: thesis: verum