let M be Pnet; ( 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; verum