let M be Pnet; :: thesis: ( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )
set R = (Flow M) | the carrier of M;
set S = id the carrier' of M;
A1: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
A2: ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M by Th12;
A3: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
A4: (f_escape M) * (f_escape M) = (((Flow M) | the carrier of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A1, A2, A3, Th11
.= f_escape M ;
A5: (f_escape M) * (f_entrance M) = f_escape M
proof
set T = ((Flow M) ~) | the carrier of M;
A6: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
A7: ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M by Th12;
A8: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_escape M) * (f_entrance M) = (((Flow M) | the carrier of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A6, A7, A8, Th11
.= f_escape M ;
hence (f_escape M) * (f_entrance M) = f_escape M ; :: thesis: verum
end;
A9: (f_entrance M) * (f_entrance M) = f_entrance M
proof
set R = ((Flow M) ~) | the carrier of M;
A10: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
A11: (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M by Th12;
A12: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_entrance M) * (f_entrance M) = ((((Flow M) ~) | the carrier of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A10, A11, A12, Th11
.= f_entrance M ;
hence (f_entrance M) * (f_entrance M) = f_entrance M ; :: thesis: verum
end;
(f_entrance M) * (f_escape M) = f_entrance M
proof
set T = ((Flow M) ~) | the carrier of M;
A13: (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M by Th12;
A14: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
A15: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_entrance M) * (f_escape M) = ((((Flow M) ~) | the carrier of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A13, A14, A15, Th11
.= f_entrance M ;
hence (f_entrance M) * (f_escape M) = f_entrance M ; :: thesis: verum
end;
hence ( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M ) by A4, A5, A9; :: thesis: verum