let x, y be object ; for M being Pnet holds
( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
let M be Pnet; ( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
A1:
the carrier of M misses the carrier' of M
by NET_1:def 2;
Flow M c= [: the carrier of M, the carrier' of M:] \/ [: the carrier' of M, the carrier of M:]
by NET_1:def 2;
hence
( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
by A1, SYSREL:7; verum