let x, y be object ; :: thesis: for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds

( x in e_Transitions N & y in e_Places N )

let N be e_net; :: thesis: ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) )

A1: ( [x,y] in the escape of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )

( x in e_Transitions N & y in e_Places N )

let N be e_net; :: thesis: ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) )

A1: ( [x,y] in the escape of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )

proof

( [x,y] in the entrance of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
the escape of N * ( the escape of N \ (id the carrier of N)) = {}
by Def2;

then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;

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

then A3: (dom the escape of N) \ (dom (CL the escape of N)) c= the carrier of N \ (dom (CL the escape of N)) by XBOOLE_1:33;

assume A4: ( [x,y] in the escape of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )

A5: the escape of N * the escape of N = the escape of N by Def1;

then x in (dom the escape of N) \ (dom (CL the escape of N)) by A4, A2, SYSREL:30;

then x in the carrier of N \ (dom (CL the escape of N)) by A3;

then A6: x in the carrier of N \ (rng the escape of N) by Th13;

y in dom (CL the escape of N) by A4, A5, A2, SYSREL:30;

then y in rng the escape of N by Th13;

hence ( x in e_Transitions N & y in e_Places N ) by A6, Th13; :: thesis: verum

end;then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;

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

then A3: (dom the escape of N) \ (dom (CL the escape of N)) c= the carrier of N \ (dom (CL the escape of N)) by XBOOLE_1:33;

assume A4: ( [x,y] in the escape of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )

A5: the escape of N * the escape of N = the escape of N by Def1;

then x in (dom the escape of N) \ (dom (CL the escape of N)) by A4, A2, SYSREL:30;

then x in the carrier of N \ (dom (CL the escape of N)) by A3;

then A6: x in the carrier of N \ (rng the escape of N) by Th13;

y in dom (CL the escape of N) by A4, A5, A2, SYSREL:30;

then y in rng the escape of N by Th13;

hence ( x in e_Transitions N & y in e_Places N ) by A6, Th13; :: thesis: verum

proof

hence
( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
by A1; :: thesis: verum
the entrance of N * ( the entrance of N \ (id the carrier of N)) = {}
by Def2;

then A7: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;

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

then A8: (dom the entrance of N) \ (dom (CL the entrance of N)) c= the carrier of N \ (dom (CL the entrance of N)) by XBOOLE_1:33;

assume A9: ( [x,y] in the entrance of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )

A10: the entrance of N * the entrance of N = the entrance of N by Def1;

then x in (dom the entrance of N) \ (dom (CL the entrance of N)) by A9, A7, SYSREL:30;

then A11: x in the carrier of N \ (dom (CL the entrance of N)) by A8;

y in dom (CL the entrance of N) by A9, A10, A7, SYSREL:30;

hence ( x in e_Transitions N & y in e_Places N ) by A11, Th13; :: thesis: verum

end;then A7: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;

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

then A8: (dom the entrance of N) \ (dom (CL the entrance of N)) c= the carrier of N \ (dom (CL the entrance of N)) by XBOOLE_1:33;

assume A9: ( [x,y] in the entrance of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )

A10: the entrance of N * the entrance of N = the entrance of N by Def1;

then x in (dom the entrance of N) \ (dom (CL the entrance of N)) by A9, A7, SYSREL:30;

then A11: x in the carrier of N \ (dom (CL the entrance of N)) by A8;

y in dom (CL the entrance of N) by A9, A10, A7, SYSREL:30;

hence ( x in e_Transitions N & y in e_Places N ) by A11, Th13; :: thesis: verum