let M be Pnet; :: thesis: ( ((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) ~ )
set R = Flow M;
Flow M c= [:(Elements M),(Elements M):] by Th8;
then ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M by SYSREL:9;
hence ( ((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) ~ ) by RELAT_1:23; :: thesis: verum