:: Some Elementary Notions of the Theory of Petri Nets
::  by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, NET_1,
      STRUCT_0, PETRI;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, PARTIT_2,
      STRUCT_0, PETRI;
 constructors TARSKI, SUBSET_1, RELAT_1, STRUCT_0, PETRI, PARTIT_2;
 registrations XBOOLE_0, SUBSET_1, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions XBOOLE_0;
 theorems TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1;
 schemes XBOOLE_0, SUBSET_1;

begin

:::definition
:::  struct(2-sorted) PT_net_Str (# carrier, carrier' -> set, Flow -> Relation #);
:::end;

definition let P be PT_net_Str;
 func Flow P 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;

::The above definition describes a "structure  of a Petri net" which
::is a kind of relational system.

reserve x,y for set;
reserve N for PT_net_Str;

definition
  let N be PT_net_Str;
  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;

:: A Petri net is defined as a triple of the form
::        N = (carrier, carrier', Flow)
:: with carrier and carrier' being disjoint sets and
::   Flow c= (carrier' x carrier) U (carrier x carrier')
:: It is allowed that both sets carrier and carrier' are empty.
:: A Petri net is here described as a predicate defined in the set
:: (on the mode) PT_net_Str.

definition
  let N be PT_net_Str;
  func Elements(N) equals
  (the carrier of N) \/ (the carrier' of N);
  correctness;
end;

theorem
  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
  x is Element of the carrier of N & the carrier of N <> {} implies x is
  Element of Elements(N)
proof
A1: the carrier of N c= Elements(N) by XBOOLE_1:7;
  assume x is Element of the carrier of N & the carrier of N <> {};
  hence thesis by A1,TARSKI:def 3;
end;

theorem
  x is Element of the carrier' of N & the carrier' of N <> {}
  implies x is Element of Elements(N)
proof
A1: the carrier' of N c= Elements(N) by XBOOLE_1:7;
  assume x is Element of the carrier' of N & the carrier' of N <> {};
  hence thesis by A1,TARSKI:def 3;
end;

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;

:: This lemma is of rather "technical" nature. It allows a definition
:: of a "subtype" of the type PT_net_Str. (see the following definition of the
:: type Pnet).

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;

:: The above definition defines a Petri net as a TYPE of the structure
:: PT_net_Str. The type is not empty.

theorem Th4:
  for N being Pnet holds not (x in the carrier of N & x in the carrier' of N)
proof
  let N be Pnet;
  (the carrier of N) misses (the carrier' of N) by Def2;
  hence thesis by XBOOLE_0:3;
end;

:: This lemma is of rather "technical" character. It will be used in the
:: proof of the correctness of a definition of a function bellow. (See
:: the definition of the functions Enter and Exit.)

theorem Th5:
  for N being 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 Th6:
  for N being 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
  for N being 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
  for N being 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;

  pred pre N,x,y means
  :Def4:
  [y,x] in Flow N & x in the carrier' of N;
  pred post N,x,y means
  :Def5:
  [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);
  func Pre(N,x) means
  :Def6:
  y in it iff y in Elements(N) & [y,x] in Flow N;
  existence
  proof
    defpred P[set] means [$1,x] in Flow N;
    thus ex IT being set st for y being set 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: y in X iff y in Elements(N) & [y,x] in Flow N and
A2: y in Y iff y in Elements(N) & [y,x] in Flow N;
A3: y in Y implies y in X
    proof
      assume y in Y;
      then y in Elements(N) & [y,x] in Flow N by A2;
      hence thesis by A1;
    end;
    y in X implies y in Y
    proof
      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:1;
  end;
  func Post(N,x) means
  :Def7:
  y in it iff y in Elements(N) & [x,y] in Flow N;
  existence
  proof
    defpred P[set] means [x,$1] in Flow N;
    thus ex IT being set st for y being set 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: y in X iff y in Elements(N) & [x,y] in Flow N and
A5: y in Y iff y in Elements(N) & [x,y] in Flow N;
A6: y in Y implies y in X
    proof
      assume y in Y;
      then y in Elements(N) & [x,y] in Flow N by A5;
      hence thesis by A4;
    end;
    y in X implies y in Y
    proof
      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:1;
  end;
end;

theorem Th9:
  for N being Pnet for x being 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 holds y in Pre(N,x) implies y in Elements(N) by Def6;
  hence thesis by TARSKI:def 3;
end;

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

theorem Th11:
  for N being Pnet for x being 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 holds y in Post(N,x) implies y in Elements(N) by Def7;
  hence thesis by TARSKI:def 3;
end;

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

theorem
  for N being Pnet for y being 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 by Def4;
    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
  proof
    assume x in Pre(N,y);
    then [x,y] in Flow N by Def6;
    hence thesis by A1,Def4;
  end;
  hence thesis by A2;
end;

theorem
  for N being Pnet for y being 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 by Def5;
    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
  proof
    assume x in Post(N,y);
    then [y,x] in Flow N by Def7;
    hence thesis by A1,Def5;
  end;
  hence thesis by A2;
end;

definition
  let N be Pnet;
  let x be Element of Elements(N);
  assume
A1: Elements(N) <> {};
  func enter(N,x) 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 Th15:
  for N being Pnet for x being 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 Th16:
  for N being Pnet for x being 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 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
  for N being Pnet for x being 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) <> {};
  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 Th18:
  for N being Pnet for x being 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 Th19:
  for N being Pnet for x being 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 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
  for N being Pnet for x being 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);
  func field(N,x) 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;
  func Prec(N,x) means
  y in it iff y in the carrier of N & [y,x] in Flow N;
  existence
  proof
    defpred P[set] means [$1,x] in Flow N;
    thus ex IT being set st for y being set 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: y in X iff y in the carrier of N & [y,x] in Flow N and
A2: y in Y iff y in the carrier of N & [y,x] in Flow N;
A3: y in Y implies y in X
    proof
      assume y in Y;
      then y in the carrier of N & [y,x] in Flow N by A2;
      hence thesis by A1;
    end;
    y in X implies y in Y
    proof
      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:1;
  end;
  func Postc(N,x) means
  y in it iff y in the carrier of N & [x,y] in Flow N;
  existence
  proof
    defpred P[set] means [x,$1] in Flow N;
    thus ex IT being set st for y being set 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: y in X iff y in the carrier of N & [x,y] in Flow N and
A5: y in Y iff y in the carrier of N & [x,y] in Flow N;
A6: y in Y implies y in X
    proof
      assume y in Y;
      then y in the carrier of N & [x,y] in Flow N by A5;
      hence thesis by A4;
    end;
    y in X implies y in Y
    proof
      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:1;
  end;
end;

definition
  let N be Pnet;
  let X be set;
  func Entr(N,X) means
  :Def13:
  x in it iff x c= Elements N & ex y being
  Element of Elements N st y in X & x = enter(N,y);
  existence
  proof
    defpred P[set] means ex y being Element of Elements N st y in X & $1 =
    enter(N,y);
    consider F being Subset-Family of Elements N such that
A1: for x being 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 being 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 being Element of
    Elements(N) st y in X & x = enter(N,y);
A4: x in Y implies x in W
    proof
      assume x in Y;
      then
      x c= Elements N & ex y being Element of Elements(N) st y in X & x =
      enter(N, y) by A3;
      hence thesis by A2;
    end;
    x in W implies x in Y
    proof
      assume x in W;
      then
      x c= Elements N & ex y being Element of Elements(N) st y in X & x =
      enter(N, y) by A2;
      hence thesis by A3;
    end;
    hence thesis by A4,TARSKI:1;
  end;
  func Ext(N,X) means
  :Def14:
  x in it iff x c= Elements N & ex y being Element
  of Elements N st y in X & x = exit(N,y);
  existence
  proof
    defpred P[set] means ex y being Element of Elements N st y in X & $1 =
    exit(N,y);
    consider F being Subset-Family of Elements N such that
A5: for x being 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 being 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 being Element of
    Elements(N) st y in X & x = exit(N,y);
A8: x in Y implies x in W
    proof
      assume x in Y;
      then
      x c= Elements N & ex y being Element of Elements(N) st y in X & x =
      exit(N,y ) by A7;
      hence thesis by A6;
    end;
    x in W implies x in Y
    proof
      assume x in W;
      then
      x c= Elements N & ex y being Element of Elements(N) st y in X & x =
      exit(N,y ) by A6;
      hence thesis by A7;
    end;
    hence thesis by A8,TARSKI:1;
  end;
end;

theorem Th21:
  for N being Pnet for x being Element of Elements(N) for X being
  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 Th22:
  for N being Pnet for x being Element of Elements(N) for X being
  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;
  func Input(N,X) equals
  union Entr(N,X);
  correctness;
  func Output(N,X) equals
  union Ext(N,X);
  correctness;
end;

theorem
  for N being Pnet for x for X being set holds X c= Elements(N) implies
(x in Input(N,X) iff ex y being 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 being Element of Elements(N) st y in X & x
  in enter(N,y)
  proof
    assume x in Input(N,X);
    then consider y being set such that
A2: x in y and
A3: y in Entr(N,X) by TARSKI:def 4;
    ex z being 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 being Element of Elements(N) st y in X & x in enter(N,y)) implies
  x in Input(N,X)
  proof
    given y being 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
  for N being Pnet for x for X being set holds X c= Elements(N) implies
(x in Output(N,X) iff ex y being 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 being Element of Elements(N) st y in X & x
  in exit(N,y)
  proof
    assume x in Output(N,X);
    then consider y being set such that
A2: x in y and
A3: y in Ext(N,X) by TARSKI:def 4;
    ex z being 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 being Element of Elements(N) st y in X & x in exit(N,y)) implies x
  in Output(N,X)
  proof
    given y being 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
  for N being Pnet for X being Subset of Elements(N) for x being 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 being 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 being 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 being 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 being 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,Def4;
      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 being 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 being
  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 being set st x in y & y in Entr(N,X) by TARSKI:def 4;
    then consider y being set such that
A12: y in Entr(N,X) and
A13: x in y;
    consider z being 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 being 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,Def4;
    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
  for N being Pnet for X being Subset of Elements(N) for x being 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 being 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 being 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 being 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 being 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,Def5;
      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 being 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 being
  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 being set st x in y & y in Ext(N,X) by TARSKI:def 4;
    then consider y being set such that
A12: y in Ext(N,X) and
A13: x in y;
    consider z being 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 being 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,Def5;
    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;