theorem Th13: :: FF_SIEC:13

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) )