let N be e_net; :: thesis: ( (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) = the escape 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)) = the entrance of N \ (id the carrier of N) )
set T = the entrance of N;
set C = the carrier of N;
set E = the escape of N;
set I = id the carrier of N;
for x, y being set st [x,y] in the escape of N \ (id the carrier of N) holds
[x,y] in (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))

proof

let x, y be set ; :: thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) )
assume A1: [x,y] in the escape of N \ (id the carrier of N) ; :: thesis: [x,y] in (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N))
then [x,y] in the escape of N by XBOOLE_0:def 5;
then A2: x in dom the escape of N by RELAT_1:def 4;
A3: not x in rng the escape of N

proof

assume x in rng the escape of N ; :: thesis: contradiction
then ex z being set st [z,x] in the escape of N by RELAT_1:def 5;
then the escape of N * (the escape of N \ (id the carrier of N)) <> {} by A1, RELAT_1:def 8;
hence contradiction by Def3; :: thesis: verum

end;

dom the escape of N c= the carrier of N by Th19;
then x in the carrier of N \ (rng the escape of N) by A2, A3, XBOOLE_0:def 5;
then [x,x] in id (the carrier of N \ (rng the escape of N)) by RELAT_1:def 10;
hence [x,y] in (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) by A1, RELAT_1:def 8; :: thesis: verum

end;

then A4: the escape of N \ (id the carrier of N) c= (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) by RELAT_1:def 3;
for x, y being set st [x,y] in the entrance of N \ (id the carrier of N) holds
[x,y] in (id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))

proof

let x, y be set ; :: thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in (id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N)) )
assume A5: [x,y] in the entrance of N \ (id the carrier of N) ; :: thesis: [x,y] in (id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N))
then [x,y] in the entrance of N by XBOOLE_0:def 5;
then A6: x in dom the entrance of N by RELAT_1:def 4;
A7: not x in rng the entrance of N

proof

assume x in rng the entrance of N ; :: thesis: contradiction
then ex z being set st [z,x] in the entrance of N by RELAT_1:def 5;
then the entrance of N * (the entrance of N \ (id the carrier of N)) <> {} by A5, RELAT_1:def 8;
hence contradiction by Def3; :: thesis: verum

end;

dom the entrance of N c= the carrier of N by Th19;
then x in the carrier of N \ (rng the entrance of N) by A6, A7, XBOOLE_0:def 5;
then [x,x] in id (the carrier of N \ (rng the entrance of N)) by RELAT_1:def 10;
hence [x,y] in (id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N)) by A5, RELAT_1:def 8; :: thesis: verum

end;

then A8: the entrance 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:def 3;
( (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) c= the escape 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)) c= the entrance of N \ (id the carrier of N) ) by RELAT_1:76;
hence ( (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) = the escape 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)) = the entrance of N \ (id the carrier of N) ) by A4, A8, XBOOLE_0:def 10; :: thesis: verum