let x, y be set ; :: thesis: for M being Pnet holds
( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) )
let M be Pnet; :: thesis: ( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) )
A1: the Places of M misses the Transitions of M by NET_1:def 1;
the Flow of M c= [:the Places of M,the Transitions of M:] \/ [:the Transitions of M,the Places of M:] by NET_1:def 1;
hence ( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) ) by A1, SYSREL:22; :: thesis: verum