consider fs1 being set such that
A1: fs1 in R1 by XBOOLE_0:def 1;
consider fs2 being set such that
A2: fs2 in R2 by XBOOLE_0:def 1;
reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;
reconsider C = fs1 ^ fs2 as firing-sequence of N ;
A3: C = fs1 \/ ((len fs1) Shift fs2) by Th64;
A4: fs1 misses (len fs1) Shift fs2 by Th65;
A5: fs1 = Seq fs1 by FINSEQ_3:125;
Seq ((len fs1) Shift fs2) in R2 by A2, Th61;
then C in R1 concur R2 by A1, A3, A4, A5;
hence not R1 concur R2 is empty ; :: thesis: verum