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 ;
then A4: not z in rng the entrance of N by XBOOLE_0:def 5;
[x,z] in the entrance of N by ;
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 ;
then A7: not z in rng the escape of N by XBOOLE_0:def 5;
[x,z] in the escape of N by ;
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 ; :: thesis: verum