theorem Th16: :: FF_SIEC:16

for M being Pnet holds
( ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M & ((Flow M) | the carrier' of M) \/ ((Flow M) | the carrier of M) = Flow M & (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) = (Flow M) ~ & (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) = (Flow M) ~ )