let N be e_net; :: thesis: ( (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 )

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: verum

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: verum