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:15, 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:29, 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 Th25;
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:29, 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 Th28;
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:6
.=
{}
;
A5:
id ( the carrier of N \ (rng the escape of N)) c= id the carrier of N
by SYSREL:15, 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:29, 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 Th28;
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:29, XBOOLE_1:36;
then
(( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= {}
by Th25;
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:6
.=
{}
;
hence
( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
by A4; verum