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 ) )
proof
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;
( [x,y] in the entrance of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
proof
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;
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