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 = the Flow of M | the Places of M;
set S = id the Transitions of M;
A1: (id the Transitions of M) * (the Flow of M | the Places of M) = {} by Th17;
A2: (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M by Th17;
A3: (id the Transitions of M) * (id the Transitions of M) = id the Transitions of M by SYSREL:29;
A4: (f_escape M) * (f_escape M) = ((the Flow of M | the Places of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) \/ ((id the Transitions of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) by SYSREL:20
.= (((the Flow of M | the Places of M) * (the Flow of M | the Places of M)) \/ ((the Flow of M | the Places of M) * (id the Transitions of M))) \/ ((id the Transitions of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) by RELAT_1:51
.= (((the Flow of M | the Places of M) * (the Flow of M | the Places of M)) \/ ((the Flow of M | the Places of M) * (id the Transitions of M))) \/ (((id the Transitions of M) * (the Flow of M | the Places of M)) \/ ((id the Transitions of M) * (id the Transitions of M))) by RELAT_1:51
.= ({} \/ (the Flow of M | the Places of M)) \/ ({} \/ (id the Transitions of M)) by A1, A2, A3, Th16
.= f_escape M ;
A5: (f_escape M) * (f_entrance M) = f_escape M

proof

set T = (the Flow of M ~ ) | the Places of M;
A6: (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} by Th17;
A7: (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M by Th17;
A8: (id the Transitions of M) * (id the Transitions of M) = id the Transitions of M by SYSREL:29;
(f_escape M) * (f_entrance M) = ((the Flow of M | the Places of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) \/ ((id the Transitions of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) by SYSREL:20
.= (((the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M)) \/ ((the Flow of M | the Places of M) * (id the Transitions of M))) \/ ((id the Transitions of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) by RELAT_1:51
.= (((the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M)) \/ ((the Flow of M | the Places of M) * (id the Transitions of M))) \/ (((id the Transitions of M) * ((the Flow of M ~ ) | the Places of M)) \/ ((id the Transitions of M) * (id the Transitions of M))) by RELAT_1:51
.= ({} \/ (the Flow of M | the Places of M)) \/ ({} \/ (id the Transitions of M)) by A6, A7, A8, Th16
.= 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 = (the Flow of M ~ ) | the Places of M;
A10: (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} by Th17;
A11: ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M by Th17;
A12: (id the Transitions of M) * (id the Transitions of M) = id the Transitions of M by SYSREL:29;
(f_entrance M) * (f_entrance M) = (((the Flow of M ~ ) | the Places of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) \/ ((id the Transitions of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) by SYSREL:20
.= ((((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Transitions of M))) \/ ((id the Transitions of M) * (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M))) by RELAT_1:51
.= ((((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Transitions of M))) \/ (((id the Transitions of M) * ((the Flow of M ~ ) | the Places of M)) \/ ((id the Transitions of M) * (id the Transitions of M))) by RELAT_1:51
.= ({} \/ ((the Flow of M ~ ) | the Places of M)) \/ ({} \/ (id the Transitions of M)) by A10, A11, A12, Th16
.= 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 = (the Flow of M ~ ) | the Places of M;
A13: ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M by Th17;
A14: (id the Transitions of M) * (the Flow of M | the Places of M) = {} by Th17;
A15: (id the Transitions of M) * (id the Transitions of M) = id the Transitions of M by SYSREL:29;
(f_entrance M) * (f_escape M) = (((the Flow of M ~ ) | the Places of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) \/ ((id the Transitions of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) by SYSREL:20
.= ((((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Transitions of M))) \/ ((id the Transitions of M) * ((the Flow of M | the Places of M) \/ (id the Transitions of M))) by RELAT_1:51
.= ((((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M)) \/ (((the Flow of M ~ ) | the Places of M) * (id the Transitions of M))) \/ (((id the Transitions of M) * (the Flow of M | the Places of M)) \/ ((id the Transitions of M) * (id the Transitions of M))) by RELAT_1:51
.= ({} \/ ((the Flow of M ~ ) | the Places of M)) \/ ({} \/ (id the Transitions of M)) by A13, A14, A15, Th16
.= 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