petri.miz

    begin

    definition

      let A,B be non empty set;

      let r be non empty Relation of A, B;

      :: original: Element

      redefine

      mode Element of r -> Element of [:A, B:] ;

      coherence

      proof

        let a be Element of r;

        thus thesis;

      end;

    end

    definition

      struct ( 2-sorted) PT_net_Str (# the carrier, carrier' -> set,

the S-T_Arcs -> Relation of the carrier, the carrier',

the T-S_Arcs -> Relation of the carrier', the carrier #)

       attr strict strict;

    end

    definition

      let N be PT_net_Str;

      :: PETRI:def1

      attr N is with_S-T_arc means

      : Def1: the S-T_Arcs of N is non empty;

      :: PETRI:def2

      attr N is with_T-S_arc means

      : Def2: the T-S_Arcs of N is non empty;

    end

    definition

      :: PETRI:def3

      func TrivialPetriNet -> PT_net_Str equals PT_net_Str (# { {} }, { {} }, ( [#] ( { {} }, { {} })), ( [#] ( { {} }, { {} })) #);

      coherence ;

    end

    registration

      cluster TrivialPetriNet -> with_S-T_arc with_T-S_arc strict non empty non void;

      coherence ;

    end

    registration

      cluster non empty non void with_S-T_arc with_T-S_arc strict for PT_net_Str;

      existence

      proof

        take TrivialPetriNet ;

        thus thesis;

      end;

    end

    registration

      let N be with_S-T_arc PT_net_Str;

      cluster the S-T_Arcs of N -> non empty;

      coherence by Def1;

    end

    registration

      let N be with_T-S_arc PT_net_Str;

      cluster the T-S_Arcs of N -> non empty;

      coherence by Def2;

    end

    definition

      mode Petri_net is non empty non void with_S-T_arc with_T-S_arc PT_net_Str;

    end

    reserve PTN for Petri_net;

    definition

      let PTN;

      mode place of PTN is Element of the carrier of PTN;

      mode places of PTN is Element of the carrier of PTN;

      mode transition of PTN is Element of the carrier' of PTN;

      mode transitions of PTN is Element of the carrier' of PTN;

      mode S-T_arc of PTN is Element of the S-T_Arcs of PTN;

      mode T-S_arc of PTN is Element of the T-S_Arcs of PTN;

    end

    definition

      let PTN;

      let x be S-T_arc of PTN;

      :: original: `1

      redefine

      func x `1 -> place of PTN ;

      coherence

      proof

        thus (x `1 ) is place of PTN;

      end;

      :: original: `2

      redefine

      func x `2 -> transition of PTN ;

      coherence

      proof

        thus (x `2 ) is transition of PTN;

      end;

    end

    definition

      let PTN;

      let x be T-S_arc of PTN;

      :: original: `1

      redefine

      func x `1 -> transition of PTN ;

      coherence

      proof

        thus (x `1 ) is transition of PTN;

      end;

      :: original: `2

      redefine

      func x `2 -> place of PTN ;

      coherence

      proof

        thus (x `2 ) is place of PTN;

      end;

    end

    reserve S0 for Subset of the carrier of PTN;

    definition

      let PTN, S0;

      :: PETRI:def4

      func *' S0 -> Subset of the carrier' of PTN equals { t where t be transition of PTN : ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [t, s] };

      coherence

      proof

        defpred P[ set] means ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [$1, s];

        { t where t be transition of PTN : P[t] } is Subset of the carrier' of PTN from DOMAIN_1:sch 7;

        hence thesis;

      end;

      correctness ;

      :: PETRI:def5

      func S0 *' -> Subset of the carrier' of PTN equals { t where t be transition of PTN : ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, t] };

      coherence

      proof

        defpred P[ set] means ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, $1];

        { t where t be transition of PTN : P[t] } is Subset of the carrier' of PTN from DOMAIN_1:sch 7;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: PETRI:1

    ( *' S0) = { (f `1 ) where f be T-S_arc of PTN : (f `2 ) in S0 }

    proof

      thus ( *' S0) c= { (f `1 ) where f be T-S_arc of PTN : (f `2 ) in S0 }

      proof

        let x be object;

        assume x in ( *' S0);

        then

        consider t be transition of PTN such that

         A1: x = t and

         A2: ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [t, s];

        consider f be T-S_arc of PTN, s be place of PTN such that

         A3: s in S0 and

         A4: f = [t, s] by A2;

        (f `1 ) = t & (f `2 ) = s by A4;

        hence thesis by A1, A3;

      end;

      let x be object;

      assume x in { (f `1 ) where f be T-S_arc of PTN : (f `2 ) in S0 };

      then

      consider f be T-S_arc of PTN such that

       A5: x = (f `1 ) & (f `2 ) in S0;

      f = [(f `1 ), (f `2 )] by MCART_1: 21;

      hence thesis by A5;

    end;

    theorem :: PETRI:2



     Th2: for x be object holds x in ( *' S0) iff ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [x, s]

    proof

      let x be object;

      thus x in ( *' S0) implies ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [x, s]

      proof

        assume x in ( *' S0);

        then

        consider t be transition of PTN such that

         A1: x = t and

         A2: ex f be T-S_arc of PTN, s be place of PTN st s in S0 & f = [t, s];

        consider f be T-S_arc of PTN, s be place of PTN such that

         A3: s in S0 & f = [t, s] by A2;

        take f, s;

        thus thesis by A1, A3;

      end;

      given f be T-S_arc of PTN, s be place of PTN such that

       A4: s in S0 and

       A5: f = [x, s];

      x = (f `1 ) by A5;

      hence thesis by A4, A5;

    end;

    theorem :: PETRI:3

    (S0 *' ) = { (f `2 ) where f be S-T_arc of PTN : (f `1 ) in S0 }

    proof

      thus (S0 *' ) c= { (f `2 ) where f be S-T_arc of PTN : (f `1 ) in S0 }

      proof

        let x be object;

        assume x in (S0 *' );

        then

        consider t be transition of PTN such that

         A1: x = t and

         A2: ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, t];

        consider f be S-T_arc of PTN, s be place of PTN such that

         A3: s in S0 and

         A4: f = [s, t] by A2;

        (f `1 ) = s & (f `2 ) = t by A4;

        hence thesis by A1, A3;

      end;

      let x be object;

      assume x in { (f `2 ) where f be S-T_arc of PTN : (f `1 ) in S0 };

      then

      consider f be S-T_arc of PTN such that

       A5: x = (f `2 ) & (f `1 ) in S0;

      f = [(f `1 ), (f `2 )] by MCART_1: 21;

      hence thesis by A5;

    end;

    theorem :: PETRI:4



     Th4: for x be object holds x in (S0 *' ) iff ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, x]

    proof

      let x be object;

      thus x in (S0 *' ) implies ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, x]

      proof

        assume x in (S0 *' );

        then

        consider t be transition of PTN such that

         A1: x = t and

         A2: ex f be S-T_arc of PTN, s be place of PTN st s in S0 & f = [s, t];

        consider f be S-T_arc of PTN, s be place of PTN such that

         A3: s in S0 & f = [s, t] by A2;

        take f, s;

        thus thesis by A1, A3;

      end;

      given f be S-T_arc of PTN, s be place of PTN such that

       A4: s in S0 and

       A5: f = [s, x];

      x = (f `2 ) by A5;

      hence thesis by A4, A5;

    end;

    reserve T0 for Subset of the carrier' of PTN;

    definition

      let PTN, T0;

      :: PETRI:def6

      func *' T0 -> Subset of the carrier of PTN equals { s where s be place of PTN : ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [s, t] };

      coherence

      proof

        defpred P[ set] means ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [$1, t];

        { s where s be place of PTN : P[s] } is Subset of the carrier of PTN from DOMAIN_1:sch 7;

        hence thesis;

      end;

      correctness ;

      :: PETRI:def7

      func T0 *' -> Subset of the carrier of PTN equals { s where s be place of PTN : ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, s] };

      coherence

      proof

        defpred P[ set] means ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, $1];

        { s where s be place of PTN : P[s] } is Subset of the carrier of PTN from DOMAIN_1:sch 7;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: PETRI:5

    ( *' T0) = { (f `1 ) where f be S-T_arc of PTN : (f `2 ) in T0 }

    proof

      thus ( *' T0) c= { (f `1 ) where f be S-T_arc of PTN : (f `2 ) in T0 }

      proof

        let x be object;

        assume x in ( *' T0);

        then

        consider s be place of PTN such that

         A1: x = s and

         A2: ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [s, t];

        consider f be S-T_arc of PTN, t be transition of PTN such that

         A3: t in T0 and

         A4: f = [s, t] by A2;

        (f `1 ) = s & (f `2 ) = t by A4;

        hence thesis by A1, A3;

      end;

      let x be object;

      assume x in { (f `1 ) where f be S-T_arc of PTN : (f `2 ) in T0 };

      then

      consider f be S-T_arc of PTN such that

       A5: x = (f `1 ) & (f `2 ) in T0;

      f = [(f `1 ), (f `2 )] by MCART_1: 21;

      hence thesis by A5;

    end;

    theorem :: PETRI:6



     Th6: for x be set holds x in ( *' T0) iff ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [x, t]

    proof

      let x be set;

      thus x in ( *' T0) implies ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [x, t]

      proof

        assume x in ( *' T0);

        then

        consider s be place of PTN such that

         A1: x = s and

         A2: ex f be S-T_arc of PTN, t be transition of PTN st t in T0 & f = [s, t];

        consider f be S-T_arc of PTN, t be transition of PTN such that

         A3: t in T0 & f = [s, t] by A2;

        take f, t;

        thus thesis by A1, A3;

      end;

      given f be S-T_arc of PTN, t be transition of PTN such that

       A4: t in T0 and

       A5: f = [x, t];

      x = (f `1 ) by A5;

      hence thesis by A4, A5;

    end;

    theorem :: PETRI:7

    (T0 *' ) = { (f `2 ) where f be T-S_arc of PTN : (f `1 ) in T0 }

    proof

      thus (T0 *' ) c= { (f `2 ) where f be T-S_arc of PTN : (f `1 ) in T0 }

      proof

        let x be object;

        assume x in (T0 *' );

        then

        consider s be place of PTN such that

         A1: x = s and

         A2: ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, s];

        consider f be T-S_arc of PTN, t be transition of PTN such that

         A3: t in T0 and

         A4: f = [t, s] by A2;

        (f `1 ) = t & (f `2 ) = s by A4;

        hence thesis by A1, A3;

      end;

      let x be object;

      assume x in { (f `2 ) where f be T-S_arc of PTN : (f `1 ) in T0 };

      then

      consider f be T-S_arc of PTN such that

       A5: x = (f `2 ) & (f `1 ) in T0;

      f = [(f `1 ), (f `2 )] by MCART_1: 21;

      hence thesis by A5;

    end;

    theorem :: PETRI:8



     Th8: for x be set holds x in (T0 *' ) iff ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, x]

    proof

      let x be set;

      thus x in (T0 *' ) implies ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, x]

      proof

        assume x in (T0 *' );

        then

        consider s be place of PTN such that

         A1: x = s and

         A2: ex f be T-S_arc of PTN, t be transition of PTN st t in T0 & f = [t, s];

        consider f be T-S_arc of PTN, t be transition of PTN such that

         A3: t in T0 & f = [t, s] by A2;

        take f, t;

        thus thesis by A1, A3;

      end;

      given f be T-S_arc of PTN, t be transition of PTN such that

       A4: t in T0 and

       A5: f = [t, x];

      x = (f `2 ) by A5;

      hence thesis by A4, A5;

    end;

    theorem :: PETRI:9

    ( *' ( {} the carrier of PTN)) = {}

    proof

      set x = the Element of ( *' ( {} the carrier of PTN));

      assume not thesis;

      then x in ( *' ( {} the carrier of PTN));

      then ex t be transition of PTN st x = t & ex f be T-S_arc of PTN, s be place of PTN st s in ( {} the carrier of PTN) & f = [t, s];

      hence contradiction;

    end;

    theorem :: PETRI:10

    (( {} the carrier of PTN) *' ) = {}

    proof

      set x = the Element of (( {} the carrier of PTN) *' );

      assume not thesis;

      then x in (( {} the carrier of PTN) *' );

      then ex t be transition of PTN st x = t & ex f be S-T_arc of PTN, s be place of PTN st s in ( {} the carrier of PTN) & f = [s, t];

      hence contradiction;

    end;

    theorem :: PETRI:11

    ( *' ( {} the carrier' of PTN)) = {}

    proof

      set x = the Element of ( *' ( {} the carrier' of PTN));

      assume not thesis;

      then x in ( *' ( {} the carrier' of PTN));

      then ex s be place of PTN st x = s & ex f be S-T_arc of PTN, t be transition of PTN st t in ( {} the carrier' of PTN) & f = [s, t];

      hence contradiction;

    end;

    theorem :: PETRI:12

    (( {} the carrier' of PTN) *' ) = {}

    proof

      set x = the Element of (( {} the carrier' of PTN) *' );

      assume not thesis;

      then x in (( {} the carrier' of PTN) *' );

      then ex s be place of PTN st x = s & ex f be T-S_arc of PTN, t be transition of PTN st t in ( {} the carrier' of PTN) & f = [t, s];

      hence contradiction;

    end;

    begin

    definition

      let PTN;

      let IT be Subset of the carrier of PTN;

      :: PETRI:def8

      attr IT is Deadlock-like means ( *' IT) is Subset of (IT *' );

    end

    definition

      let IT be Petri_net;

      :: PETRI:def9

      attr IT is With_Deadlocks means ex S be Subset of the carrier of IT st S is Deadlock-like;

    end

    registration

      cluster With_Deadlocks for Petri_net;

      existence

      proof

        take PTN1 = TrivialPetriNet ;

        reconsider s = {} as place of PTN1 by TARSKI:def 1;

        reconsider t = {} as transition of PTN1 by TARSKI:def 1;



         A1: ( [#] ( { {} }, { {} })) = { [ {} , {} ]} by ZFMISC_1: 29;

        then

        reconsider stf = [ {} , {} ] as S-T_arc of PTN1 by TARSKI:def 1;

        reconsider tsf = [ {} , {} ] as T-S_arc of PTN1 by A1, TARSKI:def 1;

         { {} } c= the carrier of PTN1;

        then

        reconsider S = { {} } as Subset of the carrier of PTN1;

        take S;

        tsf = [t, s];

        then t in ( *' S);

        then {t} c= ( *' S) by ZFMISC_1: 31;

        then

         A2: {t} = ( *' S);

        stf = [s, t];

        then t in (S *' );

        hence ( *' S) is Subset of (S *' ) by A2, ZFMISC_1: 31;

      end;

    end

    begin

    definition

      let PTN;

      let IT be Subset of the carrier of PTN;

      :: PETRI:def10

      attr IT is Trap-like means (IT *' ) is Subset of ( *' IT);

    end

    definition

      let IT be Petri_net;

      :: PETRI:def11

      attr IT is With_Traps means ex S be Subset of the carrier of IT st S is Trap-like;

    end

    registration

      cluster With_Traps for Petri_net;

      existence

      proof

        take PTN1 = TrivialPetriNet ;

        reconsider s = {} as place of PTN1 by TARSKI:def 1;

        reconsider t = {} as transition of PTN1 by TARSKI:def 1;



         A1: ( [#] ( { {} }, { {} })) = { [ {} , {} ]} by ZFMISC_1: 29;

        then

        reconsider stf = [ {} , {} ] as S-T_arc of PTN1 by TARSKI:def 1;

        reconsider tsf = [ {} , {} ] as T-S_arc of PTN1 by A1, TARSKI:def 1;

         { {} } c= the carrier of PTN1;

        then

        reconsider S = { {} } as Subset of the carrier of PTN1;

        take S;

        stf = [s, t];

        then t in (S *' );

        then {t} c= (S *' ) by ZFMISC_1: 31;

        then

         A2: {t} = (S *' );

        tsf = [t, s];

        then t in ( *' S);

        hence (S *' ) is Subset of ( *' S) by A2, ZFMISC_1: 31;

      end;

    end

    definition

      let A,B be non empty set;

      let r be non empty Relation of A, B;

      :: original: ~

      redefine

      func r ~ -> non empty Relation of B, A ;

      coherence

      proof

        set x = the Element of r;

        consider y,z be object such that

         A1: x = [y, z] by RELAT_1:def 1;

         [z, y] in (r ~ ) by A1, RELAT_1:def 7;

        hence thesis;

      end;

    end

    begin

    definition

      let PTN be PT_net_Str;

      :: PETRI:def12

      func PTN .: -> strict PT_net_Str equals PT_net_Str (# the carrier of PTN, the carrier' of PTN, (the T-S_Arcs of PTN ~ ), (the S-T_Arcs of PTN ~ ) #);

      correctness ;

    end

    registration

      let PTN be Petri_net;

      cluster (PTN .: ) -> with_S-T_arc with_T-S_arc non empty non void;

      coherence

      proof

        (the T-S_Arcs of PTN ~ ) is non empty;

        hence the S-T_Arcs of (PTN .: ) is non empty;

        (the S-T_Arcs of PTN ~ ) is non empty;

        hence the T-S_Arcs of (PTN .: ) is non empty;

        thus thesis;

      end;

    end

    theorem :: PETRI:13

    ((PTN .: ) .: ) = the PT_net_Str of PTN;

    theorem :: PETRI:14

    the carrier of PTN = the carrier of (PTN .: ) & the carrier' of PTN = the carrier' of (PTN .: ) & (the S-T_Arcs of PTN ~ ) = the T-S_Arcs of (PTN .: ) & (the T-S_Arcs of PTN ~ ) = the S-T_Arcs of (PTN .: );

    definition

      let PTN;

      let S0 be Subset of the carrier of PTN;

      :: PETRI:def13

      func S0 .: -> Subset of the carrier of (PTN .: ) equals S0;

      coherence ;

    end

    definition

      let PTN;

      let s be place of PTN;

      :: PETRI:def14

      func s .: -> place of (PTN .: ) equals s;

      coherence ;

    end

    definition

      let PTN;

      let S0 be Subset of the carrier of (PTN .: );

      :: PETRI:def15

      func .: S0 -> Subset of the carrier of PTN equals S0;

      coherence ;

    end

    definition

      let PTN;

      let s be place of (PTN .: );

      :: PETRI:def16

      func .: s -> place of PTN equals s;

      coherence ;

    end

    definition

      let PTN;

      let T0 be Subset of the carrier' of PTN;

      :: PETRI:def17

      func T0 .: -> Subset of the carrier' of (PTN .: ) equals T0;

      coherence ;

    end

    definition

      let PTN;

      let t be transition of PTN;

      :: PETRI:def18

      func t .: -> transition of (PTN .: ) equals t;

      coherence ;

    end

    definition

      let PTN;

      let T0 be Subset of the carrier' of (PTN .: );

      :: PETRI:def19

      func .: T0 -> Subset of the carrier' of PTN equals T0;

      coherence ;

    end

    definition

      let PTN;

      let t be transition of (PTN .: );

      :: PETRI:def20

      func .: t -> transition of PTN equals t;

      coherence ;

    end

    reserve S for Subset of the carrier of PTN;

    theorem :: PETRI:15



     Th15: ((S .: ) *' ) = ( *' S)

    proof

      thus ((S .: ) *' ) c= ( *' S)

      proof

        let x be object;

        assume x in ((S .: ) *' );

        then

        consider f be S-T_arc of (PTN .: ), s be place of (PTN .: ) such that

         A1: s in (S .: ) and

         A2: f = [s, x] by Th4;

         [x, ( .: s)] is T-S_arc of PTN by A2, RELAT_1:def 7;

        hence thesis by A1, Th2;

      end;

      let x be object;

      assume x in ( *' S);

      then

      consider f be T-S_arc of PTN, s be place of PTN such that

       A3: s in S and

       A4: f = [x, s] by Th2;

       [(s .: ), x] is S-T_arc of (PTN .: ) by A4, RELAT_1:def 7;

      hence thesis by A3, Th4;

    end;

    theorem :: PETRI:16



     Th16: ( *' (S .: )) = (S *' )

    proof

      thus ( *' (S .: )) c= (S *' )

      proof

        let x be object;

        assume x in ( *' (S .: ));

        then

        consider f be T-S_arc of (PTN .: ), s be place of (PTN .: ) such that

         A1: s in (S .: ) and

         A2: f = [x, s] by Th2;

         [( .: s), x] is S-T_arc of PTN by A2, RELAT_1:def 7;

        hence thesis by A1, Th4;

      end;

      let x be object;

      assume x in (S *' );

      then

      consider f be S-T_arc of PTN, s be place of PTN such that

       A3: s in S and

       A4: f = [s, x] by Th4;

       [x, (s .: )] is T-S_arc of (PTN .: ) by A4, RELAT_1:def 7;

      hence thesis by A3, Th2;

    end;

    theorem :: PETRI:17

    S is Deadlock-like iff (S .: ) is Trap-like

    proof



       A1: ((S .: ) *' ) = ( *' S) by Th15;

      thus S is Deadlock-like implies (S .: ) is Trap-like by A1, Th16;

      assume ((S .: ) *' ) is Subset of ( *' (S .: ));

      hence ( *' S) is Subset of (S *' ) by A1, Th16;

    end;

    theorem :: PETRI:18

    S is Trap-like iff (S .: ) is Deadlock-like

    proof



       A1: ((S .: ) *' ) = ( *' S) by Th15;

      thus S is Trap-like implies (S .: ) is Deadlock-like by A1, Th16;

      assume ( *' (S .: )) is Subset of ((S .: ) *' );

      hence (S *' ) is Subset of ( *' S) by A1, Th16;

    end;

    theorem :: PETRI:19

    for PTN be Petri_net, t be transition of PTN, S0 be Subset of the carrier of PTN holds t in (S0 *' ) iff ( *' {t}) meets S0

    proof

      let PTN be Petri_net;

      let t be transition of PTN;

      let S0 be Subset of the carrier of PTN;

      thus t in (S0 *' ) implies ( *' {t}) meets S0

      proof

        assume t in (S0 *' );

        then

        consider f be S-T_arc of PTN, s be place of PTN such that

         A1: s in S0 and

         A2: f = [s, t] by Th4;

        t in {t} by TARSKI:def 1;

        then s in ( *' {t}) by A2;

        hence (( *' {t}) /\ S0) <> {} by A1, XBOOLE_0:def 4;

      end;

      assume (( *' {t}) /\ S0) <> {} ;

      then

      consider s be place of PTN such that

       A3: s in (( *' {t}) /\ S0) by SUBSET_1: 4;



       A4: s in S0 by A3, XBOOLE_0:def 4;

      s in ( *' {t}) by A3, XBOOLE_0:def 4;

      then

      consider f be S-T_arc of PTN, t0 be transition of PTN such that

       A5: t0 in {t} and

       A6: f = [s, t0] by Th6;

      t0 = t by A5, TARSKI:def 1;

      hence thesis by A4, A6;

    end;

    theorem :: PETRI:20

    for PTN be Petri_net, t be transition of PTN, S0 be Subset of the carrier of PTN holds t in ( *' S0) iff ( {t} *' ) meets S0

    proof

      let PTN be Petri_net;

      let t be transition of PTN;

      let S0 be Subset of the carrier of PTN;

      thus t in ( *' S0) implies ( {t} *' ) meets S0

      proof

        assume t in ( *' S0);

        then

        consider f be T-S_arc of PTN, s be place of PTN such that

         A1: s in S0 and

         A2: f = [t, s] by Th2;

        t in {t} by TARSKI:def 1;

        then s in ( {t} *' ) by A2;

        hence (( {t} *' ) /\ S0) <> {} by A1, XBOOLE_0:def 4;

      end;

      assume (( {t} *' ) /\ S0) <> {} ;

      then

      consider s be place of PTN such that

       A3: s in (( {t} *' ) /\ S0) by SUBSET_1: 4;



       A4: s in S0 by A3, XBOOLE_0:def 4;

      s in ( {t} *' ) by A3, XBOOLE_0:def 4;

      then

      consider f be T-S_arc of PTN, t0 be transition of PTN such that

       A5: t0 in {t} and

       A6: f = [t0, s] by Th8;

      t0 = t by A5, TARSKI:def 1;

      hence thesis by A4, A6;

    end;