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:40
.=
((((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: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
;
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:40
.=
(((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:40
.=
((((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:51
.=
((((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:20
.=
((((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:20
.=
((((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:72
.=
((((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:72
.=
((((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:72
.=
((((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:72
.=
((((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:41
.=
((((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:41
.=
((((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:41
.=
((((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:41
.=
(((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:54
.=
(((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:54
.=
(((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:54
.=
(((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:54
.=
(({} ~ ) \/ ((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 Def3
.=
(({} ~ ) \/ ((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 Def3
.=
(({} ~ ) \/ ({} ~ )) \/ (((the escape of N * (the entrance of N \ (id the carrier of N))) ~ ) \/ ({} ~ ))
by Th20
.=
{}
by Th20
;
(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:54
.=
(((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:51
.=
(((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:20
.=
(((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:20
.=
((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 Def2
.=
((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 Def2
.=
((the entrance of N \/ the escape of N) \/ (the entrance of N \/ (the escape of N * the escape of N))) ~
by Def2
.=
((the entrance of N \/ the escape of N) \/ (the entrance of N \/ the escape of N)) ~
by Def2
.=
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