let N be e_net; ( (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; verum