let N be e_net; ( 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):]
proof
let x,
y be
object ;
( [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)
;
[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;
verum
end;
for x, y being object st [x,y] in the escape of N \ (id the carrier of N) holds
[x,y] in [:(e_Transitions N),(e_Places N):]
proof
let x,
y be
object ;
( [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)
;
[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;
verum
end;
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; verum