for M being Pnet holds
( ((Flow M) ~) | the carrier' of M misses id (Elements M) & (Flow M) | the carrier' of M misses id (Elements M) & ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )