let M be Pnet; ( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} )
A1:
rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M)
by Th10;
A2:
rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M)
by Th10;
A3:
rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M)
by Th10;
A4:
rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M)
by Th10;
A5:
rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M)
by Th10;
A6:
rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M)
by Th10;
A7:
rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M)
by Th10;
rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M)
by Th10;
hence
( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} )
by A1, A2, A3, A4, A5, A6, A7, RELAT_1:44; verum