:: Some Elementary Notions of the Theory of Petri Nets :: by Waldemar Korczy\'nski :: :: Received August 10, 1990 :: Copyright (c) 1990-2018 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 let P be PT_net_Str; 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; ::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) -> set 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) by XBOOLE_1:7,TARSKI:def 3; theorem 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; :: 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) by Def2,XBOOLE_0:3; :: 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 [y,x] in Flow N & x in the carrier' of N; 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); func Pre(N,x) -> set means :Def6: for y being 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 being set st for y being 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 being object holds y in X iff y in Elements(N) & [y,x] in Flow N and A2: for y being object holds y in Y iff y in Elements(N) & [y,x] in Flow N; A3: for y being 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 being 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; func Post(N,x) -> set means :Def7: for y being 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 being set st for y being 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 being object holds y in X iff y in Elements(N) & [x,y] in Flow N and A5: for y being object holds y in Y iff y in Elements(N) & [x,y] in Flow N; A6: for y being 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 being 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 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 being object 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 being object 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; 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 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; 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) <> {}; 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 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 being 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 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 being 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 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) -> 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; func Prec(N,x) -> set means for y being 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 being set st for y being 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 being object holds y in X iff y in the carrier of N & [y,x] in Flow N and A2: for y being object holds y in Y iff y in the carrier of N & [y,x] in Flow N; A3: for y being 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 being 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; func Postc(N,x) -> set means for y being 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 being set st for y being 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 being object holds y in X iff y in the carrier of N & [x,y] in Flow N and A5: for y being object holds y in Y iff y in the carrier of N & [x,y] in Flow N; A6: for y being 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 being 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; func Entr(N,X) -> set 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: for x being 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 being Element of Elements(N) st y in X & x = enter(N, y) by A3; hence thesis by A2; end; for x being 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 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:2; end; func Ext(N,X) -> set 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: for x being 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 being Element of Elements(N) st y in X & x = exit(N,y ) by A7; hence thesis by A6; end; for x being 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 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:2; 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) -> set equals union Entr(N,X); correctness; func Output(N,X) -> set 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; 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; 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; 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; 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;