let M be Pnet; :: thesis: ( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] )
A1: the carrier of M c= Elements M by XBOOLE_1:7;
A2: the carrier' of M c= Elements M by XBOOLE_1:7;
then A3: [:the carrier of M,the carrier' of M:] c= [:(Elements M),(Elements M):] by A1, ZFMISC_1:119;
[:the carrier' of M,the carrier of M:] c= [:(Elements M),(Elements M):] by A1, A2, ZFMISC_1:119;
then A4: [:the carrier of M,the carrier' of M:] \/ [:the carrier' of M,the carrier of M:] c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:8;
Flow M c= [:the carrier of M,the carrier' of M:] \/ [:the carrier' of M,the carrier of M:] by NET_1:def 2;
then Flow M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
hence ( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] ) by SYSREL:16; :: thesis: verum