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

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