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

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

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

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

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

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

dom the escape of N c= the carrier of N
by Th14;
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;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

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

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

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

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

dom the entrance of N c= the carrier of N
by Th14;
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;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

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

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