let x, y be object ; :: thesis: 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; :: thesis: ( ( [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; :: thesis: verum