let N be e_net; :: thesis: ( the entrance of N \ (id the carrier of N) c= [:(),():] & the escape of N \ (id the carrier of N) c= [:(),():] )
A1: for x, y being object st [x,y] in the entrance of N \ (id the carrier of N) holds
[x,y] in [:(),():]
proof
let x, y be object ; :: thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in [:(),():] )
assume A2: [x,y] in the entrance of N \ (id the carrier of N) ; :: thesis: [x,y] in [:(),():]
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 ;
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 ;
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 [:(),():] by ; :: thesis: verum
end;
for x, y being object st [x,y] in the escape of N \ (id the carrier of N) holds
[x,y] in [:(),():]
proof
let x, y be object ; :: thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in [:(),():] )
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 [:(),():]
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 ;
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 ;
then ( x in e_Transitions N & y in e_Places N ) by A10, A9, A7, Th17;
hence [x,y] in [:(),():] by ZFMISC_1:87; :: thesis: verum
end;
hence ( the entrance of N \ (id the carrier of N) c= [:(),():] & the escape of N \ (id the carrier of N) c= [:(),():] ) by ; :: thesis: verum