let N be e_net; :: thesis: ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )

A1: for x, y being object st [x,y] in the entrance of N \ (id the carrier of N) holds

[x,y] in [:(e_Transitions N),(e_Places N):]

[x,y] in [:(e_Transitions N),(e_Places N):]

A1: for x, y being object st [x,y] in the entrance of N \ (id the carrier of N) holds

[x,y] in [:(e_Transitions N),(e_Places N):]

proof

for x, y being object st [x,y] in the escape of N \ (id the carrier of N) holds
let x, y be object ; :: thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] )

assume A2: [x,y] in the entrance of N \ (id the carrier of N) ; :: thesis: [x,y] in [:(e_Transitions N),(e_Places N):]

then [x,y] in the entrance of N by XBOOLE_0:def 5;

then A3: x in dom the entrance of N by XTUPLE_0:def 12;

not [x,y] in id the carrier of N by A2, XBOOLE_0:def 5;

then A4: ( not x in the carrier of N or x <> y ) by RELAT_1:def 10;

A5: [x,y] in the entrance of N by A2, XBOOLE_0:def 5;

then A6: y in e_Places N by XTUPLE_0:def 13;

dom the entrance of N c= the carrier of N by Th14;

then x in e_Transitions N by A5, A4, A3, Th17;

hence [x,y] in [:(e_Transitions N),(e_Places N):] by A6, ZFMISC_1:87; :: thesis: verum

end;assume A2: [x,y] in the entrance of N \ (id the carrier of N) ; :: thesis: [x,y] in [:(e_Transitions N),(e_Places N):]

then [x,y] in the entrance of N by XBOOLE_0:def 5;

then A3: x in dom the entrance of N by XTUPLE_0:def 12;

not [x,y] in id the carrier of N by A2, XBOOLE_0:def 5;

then A4: ( not x in the carrier of N or x <> y ) by RELAT_1:def 10;

A5: [x,y] in the entrance of N by A2, XBOOLE_0:def 5;

then A6: y in e_Places N by XTUPLE_0:def 13;

dom the entrance of N c= the carrier of N by Th14;

then x in e_Transitions N by A5, A4, A3, Th17;

hence [x,y] in [:(e_Transitions N),(e_Places N):] by A6, ZFMISC_1:87; :: thesis: verum

[x,y] in [:(e_Transitions N),(e_Places N):]

proof

hence
( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )
by A1, RELAT_1:def 3; :: thesis: verum
let x, y be object ; :: thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] )

A7: dom the escape of N c= the carrier of N by Th14;

assume A8: [x,y] in the escape of N \ (id the carrier of N) ; :: thesis: [x,y] in [:(e_Transitions N),(e_Places N):]

then [x,y] in the escape of N by XBOOLE_0:def 5;

then A9: x in dom the escape of N by XTUPLE_0:def 12;

not [x,y] in id the carrier of N by A8, XBOOLE_0:def 5;

then A10: ( not x in the carrier of N or x <> y ) by RELAT_1:def 10;

[x,y] in the escape of N by A8, XBOOLE_0:def 5;

then ( x in e_Transitions N & y in e_Places N ) by A10, A9, A7, Th17;

hence [x,y] in [:(e_Transitions N),(e_Places N):] by ZFMISC_1:87; :: thesis: verum

end;A7: dom the escape of N c= the carrier of N by Th14;

assume A8: [x,y] in the escape of N \ (id the carrier of N) ; :: thesis: [x,y] in [:(e_Transitions N),(e_Places N):]

then [x,y] in the escape of N by XBOOLE_0:def 5;

then A9: x in dom the escape of N by XTUPLE_0:def 12;

not [x,y] in id the carrier of N by A8, XBOOLE_0:def 5;

then A10: ( not x in the carrier of N or x <> y ) by RELAT_1:def 10;

[x,y] in the escape of N by A8, XBOOLE_0:def 5;

then ( x in e_Transitions N & y in e_Places N ) by A10, A9, A7, Th17;

hence [x,y] in [:(e_Transitions N),(e_Places N):] by ZFMISC_1:87; :: thesis: verum