theorem Th11: :: FF_SIEC:11

for M being Pnet holds
( ((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) = {} )