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:33, 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:40
.=
(((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:72
.=
(((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:41
.=
(((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:72
.=
(((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:40
.=
(((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:40
.=
(e_flow N) \/ ((((the entrance of N ~ ) \/ the escape of N) ~ ) \/ ((id the carrier of N) ~ ))
by RELAT_1:72
.=
(e_flow N) \/ ((e_flow N) ~ )
by RELAT_1:40
;
id (the carrier of N \ (rng the entrance of N)) c= id the carrier of N
by SYSREL:33, 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:49, XBOOLE_1:36;
then
(the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) c= {}
by Th20;
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:49, XBOOLE_1:36;
then
(the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= {}
by Def3;
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:49, XBOOLE_1:36;
then
(the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) c= {}
by Th20;
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:49, XBOOLE_1:36;
then
(the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) c= {}
by Def3;
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:51
.=
(((((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:51
.=
(((((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:20
.=
(((((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:20
.=
((({} \/ {} ) \/ (((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:20
.=
(({} * (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:20
.=
((((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:20
.=
{} \/ ((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N))))
by Th35
.=
{} \/ ((the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N))))
by Th18
.=
{}
by Th35
;
(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:20
.=
((((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:51
.=
((((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:51
.=
((((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:51
.=
((({} \/ {} ) \/ (((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:20
.=
({} \/ (((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:20
.=
(((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:29
.=
(((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:20
.=
(((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:51
.=
({} \/ ((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 Th35
.=
((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 Th18
.=
{} \/ ((((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 Th35
.=
((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 Th31
.=
((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 Th18
.=
((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 Th31
.=
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