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 object 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 object ; :: 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 XTUPLE_0:def 12;
A3: not x in rng the escape of N
proof
assume x in rng the escape of N ; :: thesis: contradiction
then ex z being object st [z,x] in the escape of N by XTUPLE_0:def 13;
then the escape of N * ( the escape of N \ (id the carrier of N)) <> {} by A1, RELAT_1:def 8;
hence contradiction by Def2; :: thesis: verum
end;
dom the escape of N c= the carrier of N by Th14;
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 object 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 object ; :: 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 XTUPLE_0:def 12;
A7: not x in rng the entrance of N
proof
assume x in rng the entrance of N ; :: thesis: contradiction
then ex z being object st [z,x] in the entrance of N by XTUPLE_0:def 13;
then the entrance of N * ( the entrance of N \ (id the carrier of N)) <> {} by A5, RELAT_1:def 8;
hence contradiction by Def2; :: thesis: verum
end;
dom the entrance of N c= the carrier of N by Th14;
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:50;
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