let N be e_net; :: thesis: ( () * (() \ (id ())) = {} & () * (() \ (id ())) = {} )
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 ;
(( 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 ;
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 ;
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: () * (() \ (id ())) = ((( 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
.= {} \/ {} by
.= {} ;
A5: id ( the carrier of N \ (rng the escape of N)) c= id the carrier of N by ;
(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 ;
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 ;
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;
() * (() \ (id ())) = ((( 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
.= {} \/ {} by
.= {} ;
hence ( (e_entrance N) * (() \ (id ())) = {} & () * (() \ (id ())) = {} ) by A4; :: thesis: verum