let N be e_net; ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
set P = the escape of N \ (id N);
set Q = the entrance of N \ (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));
set R = id the carrier 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;
((the entrance of N \ (id the carrier of N)) ~ ) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) c= ((the entrance of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ )
by RELAT_1:48, XBOOLE_1:36;
then
((the entrance of N \ (id the carrier of N)) ~ ) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) c= {}
by Th33;
then A2:
((the entrance of N \ (id the carrier of N)) ~ ) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) = {}
by XBOOLE_1:3;
(id (the carrier of N \ (rng the entrance of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) c= (id (the carrier of N \ (rng the entrance of N))) * ((the entrance of N \ (id the carrier of N)) ~ )
by RELAT_1:48, XBOOLE_1:36;
then
(id (the carrier of N \ (rng the entrance of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) c= {}
by Th36;
then A3:
(id (the carrier of N \ (rng the entrance of N))) * (((the entrance of N \ (id the carrier of N)) ~ ) \ (id the carrier of N)) = {}
by XBOOLE_1:3;
A4: (e_escape N) * ((e_escape N) \ (id (e_shore N))) =
(((the entrance of N \ (id the carrier 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)) \/ ((id (the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)))
by XBOOLE_1:42
.=
(((the entrance of N \ (id the carrier 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)) \/ {} )
by A1, XBOOLE_1:37
.=
{} \/ {}
by A2, A3, SYSREL:20
.=
{}
;
A5:
id (the carrier of N \ (rng the escape of N)) c= id the carrier of N
by SYSREL:33, XBOOLE_1:36;
(id (the carrier of N \ (rng the escape of N))) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) c= (id (the carrier of N \ (rng the escape of N))) * ((the escape of N \ (id N)) ~ )
by RELAT_1:48, XBOOLE_1:36;
then
(id (the carrier of N \ (rng the escape of N))) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) c= {}
by Th36;
then A6:
(id (the carrier of N \ (rng the escape of N))) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) = {}
by XBOOLE_1:3;
((the escape of N \ (id N)) ~ ) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) c= ((the escape of N \ (id N)) ~ ) * ((the escape of N \ (id N)) ~ )
by RELAT_1:48, XBOOLE_1:36;
then
((the escape of N \ (id N)) ~ ) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) c= {}
by Th33;
then A7:
((the escape of N \ (id N)) ~ ) * (((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) = {}
by XBOOLE_1:3;
(e_entrance N) * ((e_entrance N) \ (id (e_shore N))) =
(((the escape of N \ (id N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) * ((((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) \/ ((id (the carrier of N \ (rng the escape of N))) \ (id the carrier of N)))
by XBOOLE_1:42
.=
(((the escape of N \ (id N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N)))) * ((((the escape of N \ (id N)) ~ ) \ (id the carrier of N)) \/ {} )
by A5, XBOOLE_1:37
.=
{} \/ {}
by A7, A6, SYSREL:20
.=
{}
;
hence
( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
by A4; verum