let N be e_net; :: thesis:
set P = the entrance of N;
set Q = the escape of N;
set R = 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: id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
(e_adjac N) \/ ((e_adjac N) ~) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( 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:23
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:5
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( 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:24
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) ~) \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))
.= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42 ;
then A2: ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = ((( the entrance of N \/ the escape of N) \/ (( 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)) by XBOOLE_1:4
.= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id the carrier of N) by A1, XBOOLE_1:12
.= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the entrance of N \/ the escape of N)) \ (id the carrier of N)) \/ (id the carrier of N) by RELAT_1:23
.= ((( the entrance of N ~) \/ (( the escape of N \/ the entrance of N) \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ ( the escape of N \/ ( the entrance of N \/ ( the escape of N ~)))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= (((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \/ (id the carrier of N) by XBOOLE_1:39
.= (e_flow N) \/ (((( the entrance of N \/ ( the escape of N ~)) ~) ~) \/ (id the carrier of N)) by XBOOLE_1:5
.= (e_flow N) \/ (((( the entrance of N ~) \/ (( the escape of N ~) ~)) ~) \/ (id the carrier of N)) by RELAT_1:23
.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~))
.= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ;
id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
then A3: (id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N) = {} by XBOOLE_1:37;
( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;
then A4: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;
then A5: ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15;
then A6: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;
then A7: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
A8: ((e_adjac N) \ (id the carrier of N)) * (e_adjac N) = ((((( 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)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (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))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= (((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41
.= (((( 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))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((((( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= (((( 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))) * (( 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)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( 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))) * ( the entrance 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))) * ( 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)) * (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))) \/ ((id ( the carrier of N \ (rng 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)) \/ ( 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)) * ( 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)) * (id ( the carrier of N \ (rng the entrance 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 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)) \/ ( 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)) * ( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6
.= ((({} \/ {}) \/ (((id ( the carrier of N \ (rng 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)) \/ ( 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)) * ( 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)) * (id ( the carrier of N \ (rng the entrance of N)))) by A5, A6, 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)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A3, A4, A7, SYSREL:6
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42
.= ((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41
.= ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41
.= (( 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 A3, SYSREL:6
.= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) by Th13
.= {} by Th27 ;
(e_adjac N) * (e_adjac N) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * ((( 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))) * ((( 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:6
.= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( 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))) * ((( 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:32
.= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( 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))) * (( 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 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 \/ the escape of N) \ (id the carrier of N))) \/ ((( 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))) * (( 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 XBOOLE_1:42
.= (((( 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)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( 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))) * (( 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 XBOOLE_1:42
.= (((( 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)) \/ ( 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 entrance of N))) * (( 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 XBOOLE_1:42
.= (((( 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)) \/ ( 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 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 XBOOLE_1:42
.= ((((( 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))) \/ ((( 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)))) \/ ((( 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))) * (( 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: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)))) \/ ((( 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))) * (( 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 A5, A6, SYSREL:6
.= ({} \/ ((( 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))) * (( 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 A4, A7, SYSREL:6
.= ((( 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))) * (( 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)))) by SYSREL:12
.= ((( 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))))) \/ (((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)))) by SYSREL:6
.= ((( 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))))) \/ ((((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 escape 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)) * (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))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= (( 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 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 Th13
.= {} \/ ((((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 escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= (( 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 Th23
.= (( the entrance 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 entrance 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 entrance of N))) by Th23
.= e_adjac N by XBOOLE_1:42 ;
hence ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A8, A2; :: thesis: