let N be e_net; :: thesis: ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} )
A1: for x, y being object holds not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))

proof

let x, y be object ; :: thesis: not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))
assume [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) ; :: thesis: contradiction
then consider z being object such that
A2: [x,z] in the entrance of N \ (id the carrier of N) and
A3: [z,y] in id ( the carrier of N \ (rng the entrance of N)) by RELAT_1:def 8;
z in the carrier of N \ (rng the entrance of N) by A3, RELAT_1:def 10;
then A4: not z in rng the entrance of N by XBOOLE_0:def 5;
[x,z] in the entrance of N by A2, XBOOLE_0:def 5;
hence contradiction by A4, XTUPLE_0:def 13; :: thesis: verum

end;

for x, y being object holds not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))

proof

let x, y be object ; :: thesis: not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))
assume [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) ; :: thesis: contradiction
then consider z being object such that
A5: [x,z] in the escape of N \ (id the carrier of N) and
A6: [z,y] in id ( the carrier of N \ (rng the escape of N)) by RELAT_1:def 8;
z in the carrier of N \ (rng the escape of N) by A6, RELAT_1:def 10;
then A7: not z in rng the escape of N by XBOOLE_0:def 5;
[x,z] in the escape of N by A5, XBOOLE_0:def 5;
hence contradiction by A7, XTUPLE_0:def 13; :: thesis: verum

end;

hence ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} ) by A1, RELAT_1:37; :: thesis: verum