let x, y be set ; :: 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 entrance of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )

proof

assume ( [x,y] in the entrance of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )
then ( the entrance of N * the entrance of N = the entrance of N & the entrance of N * (the entrance of N \ (id the carrier of N)) = {} & [x,y] in the entrance of N & x <> y ) by Def2, Def3;
then A2: ( the entrance of N * the entrance of N = the entrance of N & the entrance of N * (the entrance of N \ (id (dom the entrance of N))) = {} & [x,y] in the entrance of N & x <> y ) by Th16;
dom the entrance of N c= the carrier of N by Th19;
then ( x in (dom the entrance of N) \ (dom (CL the entrance of N)) & (dom the entrance of N) \ (dom (CL the entrance of N)) c= the carrier of N \ (dom (CL the entrance of N)) ) by A2, SYSREL:49, XBOOLE_1:33;
then ( x in the carrier of N \ (dom (CL the entrance of N)) & y in dom (CL the entrance of N) ) by A2, SYSREL:49;
hence ( x in e_Transitions N & y in e_Places N ) by Th18; :: thesis: verum

end;

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

proof

assume ( [x,y] in the escape of N & x <> y ) ; :: thesis: ( x in e_Transitions N & y in e_Places N )
then ( the escape of N * the escape of N = the escape of N & the escape of N * (the escape of N \ (id the carrier of N)) = {} & [x,y] in the escape of N & x <> y ) by Def2, Def3;
then A3: ( the escape of N * the escape of N = the escape of N & the escape of N * (the escape of N \ (id (dom the escape of N))) = {} & [x,y] in the escape of N & x <> y ) by Th16;
dom the escape of N c= the carrier of N by Th19;
then ( x in (dom the escape of N) \ (dom (CL the escape of N)) & (dom the escape of N) \ (dom (CL the escape of N)) c= the carrier of N \ (dom (CL the escape of N)) ) by A3, SYSREL:49, XBOOLE_1:33;
then ( x in the carrier of N \ (dom (CL the escape of N)) & y in dom (CL the escape of N) ) by A3, SYSREL:49;
then ( x in the carrier of N \ (rng the escape of N) & y in rng the escape of N ) by Th18;
hence ( x in e_Transitions N & y in e_Places N ) by Th18; :: 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