let PTN be PT_net_Str ; :: thesis:
let Sd be non empty Subset of the Places of PTN; :: thesis:
thus ( Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } ) :: thesis:

proof

assume Sd is Deadlock-like ; :: thesis:
then A1: *' Sd is Subset of (Sd *' ) by PETRI:def 5;
let M0 be Boolean_marking of PTN; :: thesis:
assume A2: M0 .: Sd = {FALSE } ; :: thesis:
defpred S₁[ FinSequence of the Transitions of PTN] means ( $1 is_firable_on M0 implies (Firing $1,M0) .: Sd = {FALSE } );
A3: S₁[ <*> the Transitions of PTN] by A2, Def5;

A4: now

let Q be FinSequence of the Transitions of PTN; :: thesis:
let x be transition of PTN; :: thesis:
assume A5: S₁[Q] ; :: thesis:
thus S₁[Q ^ <*x*>] :: thesis:

proof

assume A6: Q ^ <*x*> is_firable_on M0 ; :: thesis:
then A7: <*x*> is_firable_on Firing Q,M0 by Th11;
Firing (Q ^ <*x*>),M0 = Firing <*x*>,(Firing Q,M0) by Th10;
then consider M being FinSequence of Bool_marks_of PTN such that
A8: len <*x*> = len M and
A9: Firing (Q ^ <*x*>),M0 = M /. (len M) and
A10: M /. 1 = Firing (<*x*> /. 1),(Firing Q,M0) and
for i being Element of NAT st i < len <*x*> & i > 0 holds
M /. (i + 1) = Firing (<*x*> /. (i + 1)),(M /. i) by Def5;
<*x*> /. 1 = x by FINSEQ_4:25;
then A11: Firing (Q ^ <*x*>),M0 = ((Firing Q,M0) +* ((*' {x}) --> FALSE )) +* (({x} *' ) --> TRUE ) by A8, A9, A10, FINSEQ_1:56;
x is_firable_on Firing Q,M0 by A7, Th12;
then (Firing Q,M0) .: (*' {x}) c= {TRUE } by Def2;
then (Firing Q,M0) .: (*' {x}) misses {FALSE } by XBOOLE_1:63, ZFMISC_1:17;
then A12: *' {x} misses Sd by A5, A6, Th2, Th11;
then not x in *' Sd by A1, PETRI:19;
then {x} *' misses Sd by PETRI:20;
hence (Firing (Q ^ <*x*>),M0) .: Sd = ((Firing Q,M0) +* ((*' {x}) --> FALSE )) .: Sd by A11, Th3
.= {FALSE } by A5, A6, A12, Th3, Th11 ;
:: thesis:

end;

thus for Q0 being FinSequence of the Transitions of PTN holds S₁[Q0] from FINSEQ_2:sch 2(A3, A4); :: thesis:

end;

assume A13: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } ; :: thesis:
assume *' Sd is not Subset of (Sd *' ) ; :: according to PETRI:def 5 :: thesis:
then consider t being transition of PTN such that
A14: t in *' Sd and
A15: not t in Sd *' by SUBSET_1:7;
set M0 = (the Places of PTN --> TRUE ) +* (Sd --> FALSE );
A16: [#] the Places of PTN = the Places of PTN ;
( dom (the Places of PTN --> TRUE ) = the Places of PTN & dom (Sd --> FALSE ) = Sd ) by FUNCOP_1:19;
then A17: dom ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) = the Places of PTN \/ Sd by FUNCT_4:def 1
.= the Places of PTN by A16, SUBSET_1:28 ;
( rng (the Places of PTN --> TRUE ) c= {TRUE } & rng (Sd --> FALSE ) c= {FALSE } ) by FUNCOP_1:19;
then ( rng (the Places of PTN --> TRUE ) c= BOOLEAN & rng (Sd --> FALSE ) c= BOOLEAN ) by XBOOLE_1:1;
then A18: (rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) c= BOOLEAN by XBOOLE_1:8;
rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= (rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) by FUNCT_4:18;
then rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= BOOLEAN by A18, XBOOLE_1:1;
then reconsider M0 = (the Places of PTN --> TRUE ) +* (Sd --> FALSE ) as Boolean_marking of PTN by A17, FUNCT_2:def 2;
A19: M0 .: Sd = {FALSE } by Th5;
reconsider Q = <*t*> as FinSequence of the Transitions of PTN ;
Sd misses *' {t} by A15, PETRI:19;
then A20: (the Places of PTN --> TRUE ) .: (*' {t}) = M0 .: (*' {t}) by Th3;
A21: rng (the Places of PTN --> TRUE ) c= {TRUE } by FUNCOP_1:19;
(the Places of PTN --> TRUE ) .: (*' {t}) c= rng (the Places of PTN --> TRUE ) by RELAT_1:144;
then M0 .: (*' {t}) c= {TRUE } by A20, A21, XBOOLE_1:1;
then t is_firable_on M0 by Def2;
then A22: Q is_firable_on M0 by Th12;
{t} *' meets Sd by A14, PETRI:20;
then consider s being set such that
A23: s in ({t} *' ) /\ Sd by XBOOLE_0:4;
A24: ( s in {t} *' & s in Sd ) by A23, XBOOLE_0:def 4;
then (Firing t,M0) . s = TRUE by Th6;
then TRUE in (Firing t,M0) .: Sd by A24, FUNCT_2:43;
then (Firing t,M0) .: Sd <> {FALSE } by TARSKI:def 1;
then (Firing Q,M0) .: Sd <> {FALSE } by Th13;
hence contradiction by A13, A19, A22; :: thesis: