net_1.miz

    begin

    definition

      let P be PT_net_Str;

      :: NET_1:def1

      func Flow P -> set equals (the S-T_Arcs of P \/ the T-S_Arcs of P);

      coherence ;

    end

    registration

      let P be PT_net_Str;

      cluster ( Flow P) -> Relation-like;

      coherence ;

    end

    reserve x,y for set;

    reserve N for PT_net_Str;

    definition

      let N be PT_net_Str;

      :: NET_1:def2

      attr N is Petri means

      : Def2: the carrier of N misses the carrier' of N & ( Flow N) c= ( [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]);

    end

    definition

      let N be PT_net_Str;

      :: NET_1:def3

      func Elements (N) -> set equals (the carrier of N \/ the carrier' of N);

      correctness ;

    end

    theorem :: NET_1:1

    ( Elements N) <> {} implies (x is Element of ( Elements N) implies x is Element of the carrier of N or x is Element of the carrier' of N) by XBOOLE_0:def 3;

    theorem :: NET_1:2

    x is Element of the carrier of N & the carrier of N <> {} implies x is Element of ( Elements N) by XBOOLE_1: 7, TARSKI:def 3;

    theorem :: NET_1:3

    x is Element of the carrier' of N & the carrier' of N <> {} implies x is Element of ( Elements N) by XBOOLE_1: 7, TARSKI:def 3;



     Lm1: PT_net_Str (# {} , {} , ( {} ( {} , {} )), ( {} ( {} , {} )) #) is Petri

    proof

      set N = PT_net_Str (# {} , {} , ( {} ( {} , {} )), ( {} ( {} , {} )) #);

      thus (the carrier of N /\ the carrier' of N) = {} ;

      thus thesis;

    end;

    registration

      cluster PT_net_Str (# {} , {} , ( {} ( {} , {} )), ( {} ( {} , {} )) #) -> Petri;

      coherence by Lm1;

    end

    registration

      cluster strict Petri for PT_net_Str;

      existence

      proof

         PT_net_Str (# {} , {} , ( {} ( {} , {} )), ( {} ( {} , {} )) #) is Petri;

        hence thesis;

      end;

    end

    definition

      mode Pnet is Petri PT_net_Str;

    end

    theorem :: NET_1:4



     Th4: for N be Pnet holds not (x in the carrier of N & x in the carrier' of N) by Def2, XBOOLE_0: 3;

    theorem :: NET_1:5



     Th5: for N be Pnet holds [x, y] in ( Flow N) & x in the carrier' of N implies y in the carrier of N

    proof

      let N be Pnet;

      assume that

       A1: [x, y] in ( Flow N) and

       A2: x in the carrier' of N;



       A3: not x in the carrier of N by A2, Th4;

      ( Flow N) c= ( [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]) by Def2;

      then [x, y] in [:the carrier of N, the carrier' of N:] or [x, y] in [:the carrier' of N, the carrier of N:] by A1, XBOOLE_0:def 3;

      hence thesis by A3, ZFMISC_1: 87;

    end;

    theorem :: NET_1:6



     Th6: for N be Pnet holds [x, y] in ( Flow N) & y in the carrier' of N implies x in the carrier of N

    proof

      let N be Pnet;

      assume that

       A1: [x, y] in ( Flow N) and

       A2: y in the carrier' of N;



       A3: not y in the carrier of N by A2, Th4;

      ( Flow N) c= ( [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]) by Def2;

      then [x, y] in [:the carrier of N, the carrier' of N:] or [x, y] in [:the carrier' of N, the carrier of N:] by A1, XBOOLE_0:def 3;

      hence thesis by A3, ZFMISC_1: 87;

    end;

    theorem :: NET_1:7

    for N be Pnet holds [x, y] in ( Flow N) & x in the carrier of N implies y in the carrier' of N

    proof

      let N be Pnet;

      assume that

       A1: [x, y] in ( Flow N) and

       A2: x in the carrier of N;



       A3: not x in the carrier' of N by A2, Th4;

      ( Flow N) c= ( [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]) by Def2;

      then [x, y] in [:the carrier' of N, the carrier of N:] or [x, y] in [:the carrier of N, the carrier' of N:] by A1, XBOOLE_0:def 3;

      hence thesis by A3, ZFMISC_1: 87;

    end;

    theorem :: NET_1:8

    for N be Pnet holds [x, y] in ( Flow N) & y in the carrier of N implies x in the carrier' of N

    proof

      let N be Pnet;

      assume that

       A1: [x, y] in ( Flow N) and

       A2: y in the carrier of N;



       A3: not y in the carrier' of N by A2, Th4;

      ( Flow N) c= ( [:the carrier of N, the carrier' of N:] \/ [:the carrier' of N, the carrier of N:]) by Def2;

      then [x, y] in [:the carrier' of N, the carrier of N:] or [x, y] in [:the carrier of N, the carrier' of N:] by A1, XBOOLE_0:def 3;

      hence thesis by A3, ZFMISC_1: 87;

    end;

    definition

      let N be Pnet;

      let x, y;

      :: NET_1:def4

      pred pre N,x,y means [y, x] in ( Flow N) & x in the carrier' of N;

      :: NET_1:def5

      pred post N,x,y means [x, y] in ( Flow N) & x in the carrier' of N;

    end

    definition

      let N be PT_net_Str;

      let x be Element of ( Elements N);

      :: NET_1:def6

      func Pre (N,x) -> set means

      : Def6: for y be object holds y in it iff y in ( Elements N) & [y, x] in ( Flow N);

      existence

      proof

        defpred P[ object] means [$1, x] in ( Flow N);

        thus ex IT be set st for y be object holds y in IT iff y in ( Elements N) & P[y] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        let X,Y be set such that

         A1: for y be object holds y in X iff y in ( Elements N) & [y, x] in ( Flow N) and

         A2: for y be object holds y in Y iff y in ( Elements N) & [y, x] in ( Flow N);



         A3: for y be object holds y in Y implies y in X

        proof

          let y be object;

          assume y in Y;

          then y in ( Elements N) & [y, x] in ( Flow N) by A2;

          hence thesis by A1;

        end;

        for y be object holds y in X implies y in Y

        proof

          let y be object;

          assume y in X;

          then y in ( Elements N) & [y, x] in ( Flow N) by A1;

          hence thesis by A2;

        end;

        hence thesis by A3, TARSKI: 2;

      end;

      :: NET_1:def7

      func Post (N,x) -> set means

      : Def7: for y be object holds y in it iff y in ( Elements N) & [x, y] in ( Flow N);

      existence

      proof

        defpred P[ object] means [x, $1] in ( Flow N);

        thus ex IT be set st for y be object holds y in IT iff y in ( Elements N) & P[y] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        let X,Y be set such that

         A4: for y be object holds y in X iff y in ( Elements N) & [x, y] in ( Flow N) and

         A5: for y be object holds y in Y iff y in ( Elements N) & [x, y] in ( Flow N);



         A6: for y be object holds y in Y implies y in X

        proof

          let y be object;

          assume y in Y;

          then y in ( Elements N) & [x, y] in ( Flow N) by A5;

          hence thesis by A4;

        end;

        for y be object holds y in X implies y in Y

        proof

          let y be object;

          assume y in X;

          then y in ( Elements N) & [x, y] in ( Flow N) by A4;

          hence thesis by A5;

        end;

        hence thesis by A6, TARSKI: 2;

      end;

    end

    theorem :: NET_1:9



     Th9: for N be Pnet holds for x be Element of ( Elements N) holds ( Pre (N,x)) c= ( Elements N)

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      for y be object holds y in ( Pre (N,x)) implies y in ( Elements N) by Def6;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: NET_1:10

    for N be Pnet holds for x be Element of ( Elements N) holds ( Pre (N,x)) c= ( Elements N) by Th9;

    theorem :: NET_1:11



     Th11: for N be Pnet holds for x be Element of ( Elements N) holds ( Post (N,x)) c= ( Elements N)

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      for y be object holds y in ( Post (N,x)) implies y in ( Elements N) by Def7;

      hence thesis by TARSKI:def 3;

    end;

    theorem :: NET_1:12

    for N be Pnet holds for x be Element of ( Elements N) holds ( Post (N,x)) c= ( Elements N) by Th11;

    theorem :: NET_1:13

    for N be Pnet holds for y be Element of ( Elements N) holds y in the carrier' of N implies (x in ( Pre (N,y)) iff pre (N,y,x))

    proof

      let N be Pnet;

      let y be Element of ( Elements N);

      assume

       A1: y in the carrier' of N;



       A2: pre (N,y,x) implies x in ( Pre (N,y))

      proof

        assume pre (N,y,x);

        then

         A3: [x, y] in ( Flow N);

        then x in the carrier of N by A1, Th6;

        then x in ( Elements N) by XBOOLE_0:def 3;

        hence thesis by A3, Def6;

      end;

      x in ( Pre (N,y)) implies pre (N,y,x) by Def6, A1;

      hence thesis by A2;

    end;

    theorem :: NET_1:14

    for N be Pnet holds for y be Element of ( Elements N) holds y in the carrier' of N implies (x in ( Post (N,y)) iff post (N,y,x))

    proof

      let N be Pnet;

      let y be Element of ( Elements N);

      assume

       A1: y in the carrier' of N;



       A2: post (N,y,x) implies x in ( Post (N,y))

      proof

        assume post (N,y,x);

        then

         A3: [y, x] in ( Flow N);

        then x in the carrier of N by A1, Th5;

        then x in ( Elements N) by XBOOLE_0:def 3;

        hence thesis by A3, Def7;

      end;

      x in ( Post (N,y)) implies post (N,y,x) by Def7, A1;

      hence thesis by A2;

    end;

    definition

      let N be Pnet;

      let x be Element of ( Elements N);

      assume

       A1: ( Elements N) <> {} ;

      :: NET_1:def8

      func enter (N,x) -> set means

      : Def8: (x in the carrier of N implies it = {x}) & (x in the carrier' of N implies it = ( Pre (N,x)));

      existence

      proof

         not (x in the carrier of N & x in the carrier' of N) by Th4;

        hence thesis;

      end;

      uniqueness by A1, XBOOLE_0:def 3;

    end

    theorem :: NET_1:15



     Th15: for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( enter (N,x)) = {x} or ( enter (N,x)) = ( Pre (N,x))

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      assume ( Elements N) <> {} ;

      then x in the carrier of N or x in the carrier' of N by XBOOLE_0:def 3;

      hence thesis by Def8;

    end;

    theorem :: NET_1:16



     Th16: for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( enter (N,x)) c= ( Elements N)

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      assume

       A1: ( Elements N) <> {} ;



       A2: ( enter (N,x)) = {x} implies ( enter (N,x)) c= ( Elements N)

      proof

        x in ( Elements N) by A1;

        then

         A3: for y be object holds y in {x} implies y in ( Elements N) by TARSKI:def 1;

        assume ( enter (N,x)) = {x};

        hence thesis by A3, TARSKI:def 3;

      end;

      ( enter (N,x)) = {x} or ( enter (N,x)) = ( Pre (N,x)) by A1, Th15;

      hence thesis by A2, Th9;

    end;

    theorem :: NET_1:17

    for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( enter (N,x)) c= ( Elements N) by Th16;

    definition

      let N be Pnet;

      let x be Element of ( Elements N);

      assume

       A1: ( Elements N) <> {} ;

      :: NET_1:def9

      func exit (N,x) -> set means

      : Def9: (x in the carrier of N implies it = {x}) & (x in the carrier' of N implies it = ( Post (N,x)));

      existence

      proof

         not (x in the carrier of N & x in the carrier' of N) by Th4;

        hence thesis;

      end;

      uniqueness by A1, XBOOLE_0:def 3;

    end

    theorem :: NET_1:18



     Th18: for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( exit (N,x)) = {x} or ( exit (N,x)) = ( Post (N,x))

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      assume ( Elements N) <> {} ;

      then x in the carrier of N or x in the carrier' of N by XBOOLE_0:def 3;

      hence thesis by Def9;

    end;

    theorem :: NET_1:19



     Th19: for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( exit (N,x)) c= ( Elements N)

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      assume

       A1: ( Elements N) <> {} ;



       A2: ( exit (N,x)) = {x} implies ( exit (N,x)) c= ( Elements N)

      proof

        x in ( Elements N) by A1;

        then

         A3: for y be object holds y in {x} implies y in ( Elements N) by TARSKI:def 1;

        assume ( exit (N,x)) = {x};

        hence thesis by A3, TARSKI:def 3;

      end;

      ( exit (N,x)) = {x} or ( exit (N,x)) = ( Post (N,x)) by A1, Th18;

      hence thesis by A2, Th11;

    end;

    theorem :: NET_1:20

    for N be Pnet holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies ( exit (N,x)) c= ( Elements N) by Th19;

    definition

      let N be Pnet;

      let x be Element of ( Elements N);

      :: NET_1:def10

      func field (N,x) -> set equals (( enter (N,x)) \/ ( exit (N,x)));

      correctness ;

    end

    definition

      let N be PT_net_Str;

      let x be Element of the carrier' of N;

      :: NET_1:def11

      func Prec (N,x) -> set means for y be object holds y in it iff y in the carrier of N & [y, x] in ( Flow N);

      existence

      proof

        defpred P[ object] means [$1, x] in ( Flow N);

        thus ex IT be set st for y be object holds y in IT iff y in the carrier of N & P[y] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        let X,Y be set such that

         A1: for y be object holds y in X iff y in the carrier of N & [y, x] in ( Flow N) and

         A2: for y be object holds y in Y iff y in the carrier of N & [y, x] in ( Flow N);



         A3: for y be object holds y in Y implies y in X

        proof

          let y be object;

          assume y in Y;

          then y in the carrier of N & [y, x] in ( Flow N) by A2;

          hence thesis by A1;

        end;

        for y be object holds y in X implies y in Y

        proof

          let y be object;

          assume y in X;

          then y in the carrier of N & [y, x] in ( Flow N) by A1;

          hence thesis by A2;

        end;

        hence thesis by A3, TARSKI: 2;

      end;

      :: NET_1:def12

      func Postc (N,x) -> set means for y be object holds y in it iff y in the carrier of N & [x, y] in ( Flow N);

      existence

      proof

        defpred P[ object] means [x, $1] in ( Flow N);

        thus ex IT be set st for y be object holds y in IT iff y in the carrier of N & P[y] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        let X,Y be set such that

         A4: for y be object holds y in X iff y in the carrier of N & [x, y] in ( Flow N) and

         A5: for y be object holds y in Y iff y in the carrier of N & [x, y] in ( Flow N);



         A6: for y be object holds y in Y implies y in X

        proof

          let y be object;

          assume y in Y;

          then y in the carrier of N & [x, y] in ( Flow N) by A5;

          hence thesis by A4;

        end;

        for y be object holds y in X implies y in Y

        proof

          let y be object;

          assume y in X;

          then y in the carrier of N & [x, y] in ( Flow N) by A4;

          hence thesis by A5;

        end;

        hence thesis by A6, TARSKI: 2;

      end;

    end

    definition

      let N be Pnet;

      let X be set;

      :: NET_1:def13

      func Entr (N,X) -> set means

      : Def13: x in it iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( enter (N,y));

      existence

      proof

        defpred P[ set] means ex y be Element of ( Elements N) st y in X & $1 = ( enter (N,y));

        consider F be Subset-Family of ( Elements N) such that

         A1: for x be Subset of ( Elements N) holds x in F iff P[x] from SUBSET_1:sch 3;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let W,Y be set such that

         A2: for x holds x in W iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( enter (N,y)) and

         A3: for x holds x in Y iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( enter (N,y));



         A4: for x be object holds x in Y implies x in W

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in Y;

          then xx c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( enter (N,y)) by A3;

          hence thesis by A2;

        end;

        for x be object holds x in W implies x in Y

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in W;

          then xx c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( enter (N,y)) by A2;

          hence thesis by A3;

        end;

        hence thesis by A4, TARSKI: 2;

      end;

      :: NET_1:def14

      func Ext (N,X) -> set means

      : Def14: x in it iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( exit (N,y));

      existence

      proof

        defpred P[ set] means ex y be Element of ( Elements N) st y in X & $1 = ( exit (N,y));

        consider F be Subset-Family of ( Elements N) such that

         A5: for x be Subset of ( Elements N) holds x in F iff P[x] from SUBSET_1:sch 3;

        take F;

        thus thesis by A5;

      end;

      uniqueness

      proof

        let W,Y be set such that

         A6: for x holds x in W iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( exit (N,y)) and

         A7: for x holds x in Y iff x c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( exit (N,y));



         A8: for x be object holds x in Y implies x in W

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in Y;

          then xx c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( exit (N,y)) by A7;

          hence thesis by A6;

        end;

        for x be object holds x in W implies x in Y

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in W;

          then xx c= ( Elements N) & ex y be Element of ( Elements N) st y in X & x = ( exit (N,y)) by A6;

          hence thesis by A7;

        end;

        hence thesis by A8, TARSKI: 2;

      end;

    end

    theorem :: NET_1:21



     Th21: for N be Pnet holds for x be Element of ( Elements N) holds for X be set holds ( Elements N) <> {} & x in X implies ( enter (N,x)) in ( Entr (N,X))

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      let X be set;

      assume that

       A1: ( Elements N) <> {} and

       A2: x in X;

      ( enter (N,x)) c= ( Elements N) by A1, Th16;

      hence thesis by A2, Def13;

    end;

    theorem :: NET_1:22



     Th22: for N be Pnet holds for x be Element of ( Elements N) holds for X be set holds ( Elements N) <> {} & x in X implies ( exit (N,x)) in ( Ext (N,X))

    proof

      let N be Pnet;

      let x be Element of ( Elements N);

      let X be set;

      assume that

       A1: ( Elements N) <> {} and

       A2: x in X;

      ( exit (N,x)) c= ( Elements N) by A1, Th19;

      hence thesis by A2, Def14;

    end;

    definition

      let N be Pnet;

      let X be set;

      :: NET_1:def15

      func Input (N,X) -> set equals ( union ( Entr (N,X)));

      correctness ;

      :: NET_1:def16

      func Output (N,X) -> set equals ( union ( Ext (N,X)));

      correctness ;

    end

    theorem :: NET_1:23

    for N be Pnet holds for x holds for X be set holds X c= ( Elements N) implies (x in ( Input (N,X)) iff ex y be Element of ( Elements N) st y in X & x in ( enter (N,y)))

    proof

      let N be Pnet;

      let x;

      let X be set;



       A1: x in ( Input (N,X)) implies ex y be Element of ( Elements N) st y in X & x in ( enter (N,y))

      proof

        assume x in ( Input (N,X));

        then

        consider y be set such that

         A2: x in y and

         A3: y in ( Entr (N,X)) by TARSKI:def 4;

        ex z be Element of ( Elements N) st z in X & y = ( enter (N,z)) by A3, Def13;

        hence thesis by A2;

      end;

      assume

       A4: X c= ( Elements N);

      (ex y be Element of ( Elements N) st y in X & x in ( enter (N,y))) implies x in ( Input (N,X))

      proof

        given y be Element of ( Elements N) such that

         A5: y in X and

         A6: x in ( enter (N,y));

        ( enter (N,y)) in ( Entr (N,X)) by A4, A5, Th21;

        hence thesis by A6, TARSKI:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: NET_1:24

    for N be Pnet holds for x holds for X be set holds X c= ( Elements N) implies (x in ( Output (N,X)) iff ex y be Element of ( Elements N) st y in X & x in ( exit (N,y)))

    proof

      let N be Pnet;

      let x;

      let X be set;



       A1: x in ( Output (N,X)) implies ex y be Element of ( Elements N) st y in X & x in ( exit (N,y))

      proof

        assume x in ( Output (N,X));

        then

        consider y be set such that

         A2: x in y and

         A3: y in ( Ext (N,X)) by TARSKI:def 4;

        ex z be Element of ( Elements N) st z in X & y = ( exit (N,z)) by A3, Def14;

        hence thesis by A2;

      end;

      assume

       A4: X c= ( Elements N);

      (ex y be Element of ( Elements N) st y in X & x in ( exit (N,y))) implies x in ( Output (N,X))

      proof

        given y be Element of ( Elements N) such that

         A5: y in X and

         A6: x in ( exit (N,y));

        ( exit (N,y)) in ( Ext (N,X)) by A4, A5, Th22;

        hence thesis by A6, TARSKI:def 4;

      end;

      hence thesis by A1;

    end;

    theorem :: NET_1:25

    for N be Pnet holds for X be Subset of ( Elements N) holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies (x in ( Input (N,X)) iff (x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x)))

    proof

      let N be Pnet;

      let X be Subset of ( Elements N);

      let x be Element of ( Elements N);



       A1: (x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x)) implies x in ( Input (N,X))

      proof



         A2: (ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x)) implies x in ( Input (N,X))

        proof

          given y be Element of ( Elements N) such that

           A3: y in X and

           A4: y in the carrier' of N and

           A5: pre (N,y,x);

           [x, y] in ( Flow N) by A5;

          then x in ( Pre (N,y)) by A4, Def6;

          then

           A6: x in ( enter (N,y)) by A4, Def8;

          ( enter (N,y)) in ( Entr (N,X)) by A3, Th21;

          hence thesis by A6, TARSKI:def 4;

        end;



         A7: x in X & x in the carrier of N implies x in ( Input (N,X))

        proof

          assume that

           A8: x in X and

           A9: x in the carrier of N;

          ( enter (N,x)) = {x} & {x} c= ( Elements N) by A9, Def8, ZFMISC_1: 31;

          then

           A10: {x} in ( Entr (N,X)) by A8, Def13;

          x in {x} by TARSKI:def 1;

          hence thesis by A10, TARSKI:def 4;

        end;

        assume x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x);

        hence thesis by A7, A2;

      end;

      assume

       A11: ( Elements N) <> {} ;

      x in ( Input (N,X)) implies x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x)

      proof

        assume x in ( Input (N,X));

        then ex y be set st x in y & y in ( Entr (N,X)) by TARSKI:def 4;

        then

        consider y be set such that

         A12: y in ( Entr (N,X)) and

         A13: x in y;

        consider z be Element of ( Elements N) such that

         A14: z in X and

         A15: y = ( enter (N,z)) by A12, Def13;



         A16: z in the carrier' of N implies y = ( Pre (N,z)) by A15, Def8;



         A17: z in the carrier' of N implies ex y be Element of ( Elements N) st y in X & y in the carrier' of N & pre (N,y,x)

        proof

          assume

           A18: z in the carrier' of N;

          take z;

           [x, z] in ( Flow N) by A13, A16, A18, Def6;

          hence thesis by A14, A18;

        end;



         A19: z in the carrier of N or z in the carrier' of N by A11, XBOOLE_0:def 3;

        z in the carrier of N implies y = {z} by A15, Def8;

        hence thesis by A13, A14, A19, A17, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: NET_1:26

    for N be Pnet holds for X be Subset of ( Elements N) holds for x be Element of ( Elements N) holds ( Elements N) <> {} implies (x in ( Output (N,X)) iff (x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x)))

    proof

      let N be Pnet;

      let X be Subset of ( Elements N);

      let x be Element of ( Elements N);



       A1: (x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x)) implies x in ( Output (N,X))

      proof



         A2: (ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x)) implies x in ( Output (N,X))

        proof

          given y be Element of ( Elements N) such that

           A3: y in X and

           A4: y in the carrier' of N and

           A5: post (N,y,x);

           [y, x] in ( Flow N) by A5;

          then x in ( Post (N,y)) by A4, Def7;

          then

           A6: x in ( exit (N,y)) by A4, Def9;

          ( exit (N,y)) in ( Ext (N,X)) by A3, Th22;

          hence thesis by A6, TARSKI:def 4;

        end;



         A7: x in X & x in the carrier of N implies x in ( Output (N,X))

        proof

          assume that

           A8: x in X and

           A9: x in the carrier of N;

          ( exit (N,x)) = {x} & {x} c= ( Elements N) by A9, Def9, ZFMISC_1: 31;

          then

           A10: {x} in ( Ext (N,X)) by A8, Def14;

          x in {x} by TARSKI:def 1;

          hence thesis by A10, TARSKI:def 4;

        end;

        assume x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x);

        hence thesis by A7, A2;

      end;

      assume

       A11: ( Elements N) <> {} ;

      x in ( Output (N,X)) implies x in X & x in the carrier of N or ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x)

      proof

        assume x in ( Output (N,X));

        then ex y be set st x in y & y in ( Ext (N,X)) by TARSKI:def 4;

        then

        consider y be set such that

         A12: y in ( Ext (N,X)) and

         A13: x in y;

        consider z be Element of ( Elements N) such that

         A14: z in X and

         A15: y = ( exit (N,z)) by A12, Def14;



         A16: z in the carrier' of N implies y = ( Post (N,z)) by A15, Def9;



         A17: z in the carrier' of N implies ex y be Element of ( Elements N) st y in X & y in the carrier' of N & post (N,y,x)

        proof

          assume

           A18: z in the carrier' of N;

          take z;

           [z, x] in ( Flow N) by A13, A16, A18, Def7;

          hence thesis by A14, A18;

        end;



         A19: z in the carrier of N or z in the carrier' of N by A11, XBOOLE_0:def 3;

        z in the carrier of N implies y = {z} by A15, Def9;

        hence thesis by A13, A14, A19, A17, TARSKI:def 1;

      end;

      hence thesis by A1;

    end;