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

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

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