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 set 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 set ; :: 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 set such that
A2: ( [x,z] in the escape of N \ (id the carrier of N) & [z,y] in id (the carrier of N \ (rng the escape of N)) ) by RELAT_1:def 8;
( [x,z] in the escape of N & z in the carrier of N \ (rng the escape of N) ) by A2, RELAT_1:def 10, XBOOLE_0:def 5;
then ( [x,z] in the escape of N & not z in rng the escape of N ) by XBOOLE_0:def 5;
hence contradiction by RELAT_1:def 5; :: thesis: verum

end;

for x, y being set 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 set ; :: 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 set such that
A3: ( [x,z] in the entrance of N \ (id the carrier of N) & [z,y] in id (the carrier of N \ (rng the entrance of N)) ) by RELAT_1:def 8;
( [x,z] in the entrance of N & z in the carrier of N \ (rng the entrance of N) ) by A3, RELAT_1:def 10, XBOOLE_0:def 5;
then ( [x,z] in the entrance of N & not z in rng the entrance of N ) by XBOOLE_0:def 5;
hence contradiction by RELAT_1:def 5; :: 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:56; :: thesis: verum