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:6
.= (((( 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:32
.= (((( 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:32
.= (((( 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:35
.= (((( 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)))))
.= (((( 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)))))
.= (((( 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:12
.= (((( 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:35
.= (((( 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:35
.= (({} ~) \/ (((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 Th24
.= (({} ~) \/ (( 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 Th23
.= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27
.= e_entrance N ;
A2: (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:6
.= (((( 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:32
.= (((( 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:32
.= (((( 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:35
.= (((( 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)))))
.= (((( 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)))))
.= (((( 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:12
.= (((( 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:35
.= (((( 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:35
.= (({} ~) \/ (((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 Th24
.= (({} ~) \/ (( 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 Th23
.= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= e_escape 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:6
.= (((( 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:32
.= (((( 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:32
.= (((( 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:35
.= (((( 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)))))
.= (((( 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)))))
.= (((( 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 Th13
.= (((( 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:12
.= (((( 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:35
.= (((( 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:35
.= (((( 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 Th13
.= (((( 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 Th13
.= (({} ~) \/ (((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 Th24
.= (({} ~) \/ (( 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 Th23
.= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= e_escape N ;
(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:6
.= (((( 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:32
.= (((( 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:32
.= (((( 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:35
.= (((( 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)))))
.= (((( 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)))))
.= (((( 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 Th13
.= (((( 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:12
.= (((( 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:35
.= (((( 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:35
.= (((( 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 Th13
.= (((( 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 Th13
.= (({} ~) \/ (((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 Th24
.= (({} ~) \/ (( 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 Th23
.= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27
.= e_entrance 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, A3, A2; :: thesis: