let P be set ; :: thesis: for N being Petri_net of P

for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

let N be Petri_net of P; :: thesis: for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

let C1, C2 be firing-sequence of N; :: thesis: {C1} before {C2} = {(C1 ^ C2)}

thus {C1} before {C2} c= {(C1 ^ C2)} :: according to XBOOLE_0:def 10 :: thesis: {(C1 ^ C2)} c= {C1} before {C2}

assume x in {(C1 ^ C2)} ; :: thesis: x in {C1} before {C2}

then A5: x = C1 ^ C2 by TARSKI:def 1;

A6: C1 in {C1} by TARSKI:def 1;

C2 in {C2} by TARSKI:def 1;

hence x in {C1} before {C2} by A5, A6; :: thesis: verum

for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

let N be Petri_net of P; :: thesis: for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

let C1, C2 be firing-sequence of N; :: thesis: {C1} before {C2} = {(C1 ^ C2)}

thus {C1} before {C2} c= {(C1 ^ C2)} :: according to XBOOLE_0:def 10 :: thesis: {(C1 ^ C2)} c= {C1} before {C2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(C1 ^ C2)} or x in {C1} before {C2} )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {C1} before {C2} or x in {(C1 ^ C2)} )

assume x in {C1} before {C2} ; :: thesis: x in {(C1 ^ C2)}

then consider fs1, fs2 being firing-sequence of N such that

A1: x = fs1 ^ fs2 and

A2: fs1 in {C1} and

A3: fs2 in {C2} ;

A4: fs1 = C1 by A2, TARSKI:def 1;

fs2 = C2 by A3, TARSKI:def 1;

hence x in {(C1 ^ C2)} by A1, A4, TARSKI:def 1; :: thesis: verum

end;assume x in {C1} before {C2} ; :: thesis: x in {(C1 ^ C2)}

then consider fs1, fs2 being firing-sequence of N such that

A1: x = fs1 ^ fs2 and

A2: fs1 in {C1} and

A3: fs2 in {C2} ;

A4: fs1 = C1 by A2, TARSKI:def 1;

fs2 = C2 by A3, TARSKI:def 1;

hence x in {(C1 ^ C2)} by A1, A4, TARSKI:def 1; :: thesis: verum

assume x in {(C1 ^ C2)} ; :: thesis: x in {C1} before {C2}

then A5: x = C1 ^ C2 by TARSKI:def 1;

A6: C1 in {C1} by TARSKI:def 1;

C2 in {C2} by TARSKI:def 1;

hence x in {C1} before {C2} by A5, A6; :: thesis: verum