theorem Th14: :: FF_SIEC:14

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