consider
fs1
being
object
such that
A1
:
fs1
in
R1
by
XBOOLE_0:def 1
;
consider
fs2
being
object
such that
A2
:
fs2
in
R2
by
XBOOLE_0:def 1
;
reconsider
fs1
=
fs1
,
fs2
=
fs2
as
firing-sequence
of
N
by
A1
,
A2
;
fs1
^
fs2
in
R1
before
R2
by
A1
,
A2
;
hence
not
R1
before
R2
is
empty
;
:: thesis:
verum