let N be e_net; ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
set R = the entrance of N;
set S = the escape of N;
set T = id the carrier of N;
A1: ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) =
((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the escape of N \/ the entrance of N)) \/ (id the carrier of N)
by RELAT_1:23
.=
(((( the entrance of N ~) \/ ( the escape of N ~)) \/ the escape of N) \/ the entrance of N) \/ (id the carrier of N)
by XBOOLE_1:4
.=
((( the entrance of N ~) \/ (( the escape of N ~) \/ the escape of N)) \/ the entrance of N) \/ (id the carrier of N)
by XBOOLE_1:4
.=
(( the entrance of N ~) \/ (( the escape of N \/ ( the escape of N ~)) \/ the entrance of N)) \/ (id the carrier of N)
by XBOOLE_1:4
.=
(( the entrance of N ~) \/ ( the escape of N \/ (( the escape of N ~) \/ the entrance of N))) \/ (id the carrier of N)
by XBOOLE_1:4
.=
((( the entrance of N ~) \/ the escape of N) \/ (( the escape of N ~) \/ the entrance of N)) \/ (id the carrier of N)
by XBOOLE_1:4
.=
(e_flow N) \/ ((( the escape of N ~) \/ (( the entrance 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
;
A2: ((e_prox N) \ (id the carrier of N)) * (e_prox N) =
((( the entrance of N ~) \/ ( the escape of N ~)) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) ~)
by RELAT_1:23
.=
((( 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) ~)
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 ~) \/ ( the escape of N ~))
by RELAT_1:23
.=
(((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the entrance of N ~)) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~))
by RELAT_1:32
.=
(((( 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 entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~))
by SYSREL:6
.=
(((( 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 entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
by SYSREL:6
.=
(((( 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 entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.=
(((( 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 entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.=
(((( 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 entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.=
(((( 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 entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))
.=
(((( 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 entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))
by RELAT_1:24
.=
(((( 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 entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))
by RELAT_1:24
.=
(((( 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 entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))
by RELAT_1:24
.=
(((( 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 entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~)))
by RELAT_1:24
.=
((( the entrance 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 entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~)))
by RELAT_1:35
.=
((( the entrance of N * ( 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 \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~)))
by RELAT_1:35
.=
((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~)))
by RELAT_1:35
.=
((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~))
by RELAT_1:35
.=
(({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~))
by Def2
.=
(({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~))
by Def2
.=
(({} ~) \/ ({} ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~))
by Th15
.=
{}
by Th15
;
(e_prox N) * (e_prox N) =
(( the entrance of N \/ the escape of N) * ( the entrance of N \/ the escape of N)) ~
by RELAT_1:35
.=
((( the entrance of N \/ the escape of N) * the entrance of N) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~
by RELAT_1:32
.=
((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~
by SYSREL:6
.=
((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~
by SYSREL:6
.=
(( the entrance of N \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~
by Def1
.=
(( the entrance of N \/ the escape of N) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~
by Def1
.=
(( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N * the escape of N))) ~
by Def1
.=
(( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ the escape of N)) ~
by Def1
.=
e_prox N
;
hence
( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
by A2, A1; verum