let N be e_net; :: thesis: ( (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; :: thesis: verum

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; :: thesis: verum