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)))

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

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)))
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;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

proof

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
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;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