let M be Pnet; :: thesis: ( the Flow of M c= [:(Elements M),(Elements M):] & the Flow of M ~ c= [:(Elements M),(Elements M):] )
A1: the Places of M c= Elements M by XBOOLE_1:7;
A2: the Transitions of M c= Elements M by XBOOLE_1:7;
then A3: [:the Places of M,the Transitions of M:] c= [:(Elements M),(Elements M):] by A1, ZFMISC_1:119;
[:the Transitions of M,the Places of M:] c= [:(Elements M),(Elements M):] by A1, A2, ZFMISC_1:119;
then A4: [:the Places of M,the Transitions of M:] \/ [:the Transitions of M,the Places of M:] c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:8;
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;
then the Flow of M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
hence ( the Flow of M c= [:(Elements M),(Elements M):] & the Flow of M ~ c= [:(Elements M),(Elements M):] ) by SYSREL:16; :: thesis: verum