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:96;
[: the carrier' of M, the carrier of M:] c= [:(Elements M),(Elements M):] by A1, A2, ZFMISC_1:96;
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:4; :: thesis: verum