let N be e_net; :: thesis:
set P = the escape of N \ (id the carrier of N);
set Q = the entrance of N \ (id the carrier of N);
set S = id (the carrier of N \ (rng the entrance of N));
set T = id (the carrier of N \ (rng the escape of N));
A1: (e_entrance N) * (e_entrance N) = (((the escape of N \ (id the carrier of N)) ~ ) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) \/ ((id (the carrier of N \ (rng the escape of N))) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) by SYSREL:20
.= ((((the escape of N \ (id the carrier of N)) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ ((id (the carrier of N \ (rng the escape of N))) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:51
.= ((((the escape of N \ (id the carrier of N)) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:51
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:54
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:72
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:72
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the escape of N)))) by SYSREL:29
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the escape of N)))) by RELAT_1:54
.= ((((the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by RELAT_1:54
.= (({} ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th32
.= (({} ~ ) \/ ((the escape of N \ (id the carrier of N)) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th31
.= ({} \/ ((the escape of N \ (id the carrier of N)) ~ )) \/ ({} \/ (id (the carrier of N \ (rng the escape of N)))) by Th35
.= e_entrance N ;
A2: (e_entrance N) * (e_escape N) = (((the escape of N \ (id the carrier of N)) ~ ) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) \/ ((id (the carrier of N \ (rng the escape of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) by SYSREL:20
.= ((((the escape of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ ((id (the carrier of N \ (rng the escape of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:51
.= ((((the escape of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:51
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:54
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ (((id (the carrier of N \ (rng the escape of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:72
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:72
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the escape of N))) * (id (the carrier of N \ (rng the escape of N))))) by Th18
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the escape of N)))) by SYSREL:29
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((id (the carrier of N \ (rng the escape of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the escape of N)))) by RELAT_1:54
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by RELAT_1:54
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th18
.= ((((the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th18
.= (({} ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th32
.= (({} ~ ) \/ ((the escape of N \ (id the carrier of N)) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) by Th31
.= ({} \/ ((the escape of N \ (id the carrier of N)) ~ )) \/ ({} \/ (id (the carrier of N \ (rng the escape of N)))) by Th35
.= e_entrance N ;
A3: (e_escape N) * (e_entrance N) = (((the entrance of N \ (id the carrier of N)) ~ ) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) \/ ((id (the carrier of N \ (rng the entrance of N))) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) by SYSREL:20
.= ((((the entrance of N \ (id the carrier of N)) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ ((id (the carrier of N \ (rng the entrance of N))) * (((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:51
.= ((((the entrance of N \ (id the carrier of N)) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:51
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the escape of N))))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:54
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:72
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the escape of N))))) by RELAT_1:72
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the entrance of N))))) by Th18
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the entrance of N)))) by SYSREL:29
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the escape of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the entrance of N)))) by RELAT_1:54
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the escape of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by RELAT_1:54
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th18
.= ((((the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th18
.= (({} ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th32
.= (({} ~ ) \/ ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th31
.= ({} \/ ((the entrance of N \ (id the carrier of N)) ~ )) \/ ({} \/ (id (the carrier of N \ (rng the entrance of N)))) by Th35
.= e_escape N ;
(e_escape N) * (e_escape N) = (((the entrance of N \ (id the carrier of N)) ~ ) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) \/ ((id (the carrier of N \ (rng the entrance of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) by SYSREL:20
.= ((((the entrance of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ ((id (the carrier of N \ (rng the entrance of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:51
.= ((((the entrance of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:51
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * (id (the carrier of N \ (rng the entrance of N))))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:54
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ (((id (the carrier of N \ (rng the entrance of N))) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:72
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((id (the carrier of N \ (rng the entrance of N))) * (id (the carrier of N \ (rng the entrance of N))))) by RELAT_1:72
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ))) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the entrance of N)))) by SYSREL:29
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((id (the carrier of N \ (rng the entrance of N))) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )) \/ (id (the carrier of N \ (rng the entrance of N)))) by RELAT_1:54
.= ((((the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N))) ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by RELAT_1:54
.= (({} ~ ) \/ (((id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th32
.= (({} ~ ) \/ ((the entrance of N \ (id the carrier of N)) ~ )) \/ ((((the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N)))) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)))) by Th31
.= ({} \/ ((the entrance of N \ (id the carrier of N)) ~ )) \/ ({} \/ (id (the carrier of N \ (rng the entrance of N)))) by Th35
.= e_escape N ;
hence ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N ) by A1, A2, A3; :: thesis: