:: NET_1 semantic presentation

begin

definition
let P be PT_net_Str ;
func Flow P ->  set  equals :: NET_1:def 1
 the S-T_Arcs of P \/ the T-S_Arcs of P;
coherence
 the S-T_Arcs of P \/ the T-S_Arcs of P is set ;
end;

:: deftheorem  defines Flow NET_1:def_1_:_
 for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P;

registration
let P be PT_net_Str ;
cluster Flow P ->  Relation-like ;
coherence
 Flow P is Relation-like ;
end;


definition
let N be PT_net_Str ;
attrN is Petri  means :Def2: :: NET_1:def 2
( 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;

:: deftheorem Def2 defines Petri NET_1:def_2_:_
 for N being PT_net_Str holds
( N is Petri iff ( 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:] ) );

definition
let N be PT_net_Str ;
func Elements N ->  set  equals :: NET_1:def 3
 the carrier of N \/ the carrier' of N;
correctness
coherence
the carrier of N \/ the carrier' of N is set ;
;
end;

:: deftheorem  defines Elements NET_1:def_3_:_
 for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;

theorem :: NET_1:1
for x being set
for N being PT_net_Str holds
( not Elements N <> {} or not x is Element of Elements N or 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
for x being set
for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds
x is Element of Elements N
proof
let x be set ; ::_thesis: for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds
x is Element of Elements N
let N be PT_net_Str ; ::_thesis: ( x is Element of the carrier of N & the carrier of N <> {} implies x is Element of Elements N )
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 <> {} ) ; ::_thesis: x is Element of Elements N
hence  x is Element of Elements N by A1, TARSKI:def_3; ::_thesis: verum
end;

theorem :: NET_1:3
for x being set
for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds
x is Element of Elements N
proof
let x be set ; ::_thesis: for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds
x is Element of Elements N
let N be PT_net_Str ; ::_thesis: ( x is Element of the carrier' of N & the carrier' of N <> {} implies x is Element of Elements N )
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 <> {} ) ; ::_thesis: x is Element of Elements N
hence  x is Element of Elements N by A1, TARSKI:def_3; ::_thesis: verum
end;

Lm1:  PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri
proof
set N = PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #);
thus  the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) /\ the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) = {} ; :: according to XBOOLE_0:def_7,NET_1:def_2 ::_thesis: Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):]
thus  Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] ; ::_thesis: verum
end;

registration
cluster PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) ->  Petri ;
coherence
 PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri by Lm1;
end;

registration
cluster strict Petri for PT_net_Str ;
existence
 ex b1 being PT_net_Str st
( b1 is strict & b1 is Petri )
proof
 PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri ;
hence  ex b1 being PT_net_Str st
( b1 is strict & b1 is Petri ) ; ::_thesis: verum
end;
end;

definition
mode Pnet is Petri PT_net_Str ;
end;

theorem Th4: :: NET_1:4
for x being set
for N being Pnet holds
( not x in the carrier of N or not x in the carrier' of N )
proof
let x be set ; ::_thesis: for N being Pnet holds
( not x in the carrier of N or not x in the carrier' of N )
let N be Pnet; ::_thesis: ( not x in the carrier of N or not x in the carrier' of N )
 the carrier of N misses the carrier' of N by Def2;
hence  ( not x in the carrier of N or not x in the carrier' of N ) by XBOOLE_0:3; ::_thesis: verum
end;

theorem Th5: :: NET_1:5
for x, y being set
for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds
y in the carrier of N
proof
let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds
y in the carrier of N
let N be Pnet; ::_thesis: ( [x,y] in Flow N & x in the carrier' of N implies y in the carrier of N )
assume that
A1: [x,y] in Flow N and
A2: x in the carrier' of N ; ::_thesis: y 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  y in the carrier of N by A3, ZFMISC_1:87; ::_thesis: verum
end;

theorem Th6: :: NET_1:6
for x, y being set
for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds
x in the carrier of N
proof
let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds
x in the carrier of N
let N be Pnet; ::_thesis: ( [x,y] in Flow N & y in the carrier' of N implies x in the carrier of N )
assume that
A1: [x,y] in Flow N and
A2: y in the carrier' of N ; ::_thesis: x 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  x in the carrier of N by A3, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: NET_1:7
for x, y being set
for N being Pnet st [x,y] in Flow N & x in the carrier of N holds
y in the carrier' of N
proof
let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & x in the carrier of N holds
y in the carrier' of N
let N be Pnet; ::_thesis: ( [x,y] in Flow N & x in the carrier of N implies y in the carrier' of N )
assume that
A1: [x,y] in Flow N and
A2: x in the carrier of N ; ::_thesis: y 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  y in the carrier' of N by A3, ZFMISC_1:87; ::_thesis: verum
end;

theorem :: NET_1:8
for x, y being set
for N being Pnet st [x,y] in Flow N & y in the carrier of N holds
x in the carrier' of N
proof
let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & y in the carrier of N holds
x in the carrier' of N
let N be Pnet; ::_thesis: ( [x,y] in Flow N & y in the carrier of N implies x in the carrier' of N )
assume that
A1: [x,y] in Flow N and
A2: y in the carrier of N ; ::_thesis: x 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  x in the carrier' of N by A3, ZFMISC_1:87; ::_thesis: verum
end;

definition
let N be Pnet;
let x, y be set ;
pred pre N,x,y means :Def4: :: NET_1:def 4
( [y,x] in Flow N & x in the carrier' of N );
pred post N,x,y means :Def5: :: NET_1:def 5
( [x,y] in Flow N & x in the carrier' of N );
end;

:: deftheorem Def4 defines pre NET_1:def_4_:_
 for N being Pnet
for x, y being set holds
( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) );

:: deftheorem Def5 defines post NET_1:def_5_:_
 for N being Pnet
for x, y being set holds
( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) );

definition
let N be PT_net_Str ;
let x be Element of Elements N;
func Pre (N,x) ->  set  means :Def6: :: NET_1:def 6
 for y being set holds
( y in it iff ( y in Elements N & [y,x] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) )
proof
defpred S1[ 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 & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [y,x] in Flow N ) ) ) holds
b1 = b2
proof
let X, Y be set ; ::_thesis: ( ( for y being set holds
( y in X iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ) implies X = Y )
assume that
A1: for y being set holds
( y in X iff ( y in Elements N & [y,x] in Flow N ) ) and
A2: for y being set holds
( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ; ::_thesis: X = Y
A3: for y being set st y in Y holds
y in X
proof
let y be set ; ::_thesis: ( y in Y implies y in X )
assume  y in Y ; ::_thesis: y in X
then  ( y in Elements N & [y,x] in Flow N ) by A2;
hence  y in X by A1; ::_thesis: verum
end;
 for y being set st y in X holds
y in Y
proof
let y be set ; ::_thesis: ( y in X implies y in Y )
assume  y in X ; ::_thesis: y in Y
then  ( y in Elements N & [y,x] in Flow N ) by A1;
hence  y in Y by A2; ::_thesis: verum
end;
hence  X = Y by A3, TARSKI:1; ::_thesis: verum
end;
func Post (N,x) ->  set  means :Def7: :: NET_1:def 7
 for y being set holds
( y in it iff ( y in Elements N & [x,y] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) )
proof
defpred S1[ 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 & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [x,y] in Flow N ) ) ) holds
b1 = b2
proof
let X, Y be set ; ::_thesis: ( ( for y being set holds
( y in X iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in Y iff ( y in Elements N & [x,y] in Flow N ) ) ) implies X = Y )
assume that
A4: for y being set holds
( y in X iff ( y in Elements N & [x,y] in Flow N ) ) and
A5: for y being set holds
( y in Y iff ( y in Elements N & [x,y] in Flow N ) ) ; ::_thesis: X = Y
A6: for y being set st y in Y holds
y in X
proof
let y be set ; ::_thesis: ( y in Y implies y in X )
assume  y in Y ; ::_thesis: y in X
then  ( y in Elements N & [x,y] in Flow N ) by A5;
hence  y in X by A4; ::_thesis: verum
end;
 for y being set st y in X holds
y in Y
proof
let y be set ; ::_thesis: ( y in X implies y in Y )
assume  y in X ; ::_thesis: y in Y
then  ( y in Elements N & [x,y] in Flow N ) by A4;
hence  y in Y by A5; ::_thesis: verum
end;
hence  X = Y by A6, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Pre NET_1:def_6_:_
 for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Pre (N,x) iff for y being set holds
( y in b3 iff ( y in Elements N & [y,x] in Flow N ) ) );

:: deftheorem Def7 defines Post NET_1:def_7_:_
 for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Post (N,x) iff for y being set holds
( y in b3 iff ( y in Elements N & [x,y] in Flow N ) ) );

theorem Th9: :: NET_1:9
for N being Pnet
for x being Element of Elements N holds Pre (N,x) c= Elements N
proof
let N be Pnet; ::_thesis: for x being Element of Elements N holds Pre (N,x) c= Elements N
let x be Element of Elements N; ::_thesis: Pre (N,x) c= Elements N
 for y being set st y in Pre (N,x) holds
y in Elements N by Def6;
hence  Pre (N,x) c= Elements N by TARSKI:def_3; ::_thesis: verum
end;

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

theorem Th11: :: NET_1:11
for N being Pnet
for x being Element of Elements N holds Post (N,x) c= Elements N
proof
let N be Pnet; ::_thesis: for x being Element of Elements N holds Post (N,x) c= Elements N
let x be Element of Elements N; ::_thesis: Post (N,x) c= Elements N
 for y being set st y in Post (N,x) holds
y in Elements N by Def7;
hence  Post (N,x) c= Elements N by TARSKI:def_3; ::_thesis: verum
end;

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

theorem :: NET_1:13
for x being set
for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Pre (N,y) iff pre N,y,x )
proof
let x be set ; ::_thesis: for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Pre (N,y) iff pre N,y,x )
let N be Pnet; ::_thesis: for y being Element of Elements N st y in the carrier' of N holds
( x in Pre (N,y) iff pre N,y,x )
let y be Element of Elements N; ::_thesis: ( y in the carrier' of N implies ( x in Pre (N,y) iff pre N,y,x ) )
assume A1: y in the carrier' of N ; ::_thesis: ( x in Pre (N,y) iff pre N,y,x )
A2: ( pre N,y,x implies x in Pre (N,y) )
proof
assume  pre N,y,x ; ::_thesis: x in Pre (N,y)
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  x in Pre (N,y) by A3, Def6; ::_thesis: verum
end;
 ( x in Pre (N,y) implies pre N,y,x )
proof
assume  x in Pre (N,y) ; ::_thesis: pre N,y,x
then  [x,y] in Flow N by Def6;
hence  pre N,y,x by A1, Def4; ::_thesis: verum
end;
hence  ( x in Pre (N,y) iff pre N,y,x ) by A2; ::_thesis: verum
end;

theorem :: NET_1:14
for x being set
for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Post (N,y) iff post N,y,x )
proof
let x be set ; ::_thesis: for N being Pnet
for y being Element of Elements N st y in the carrier' of N holds
( x in Post (N,y) iff post N,y,x )
let N be Pnet; ::_thesis: for y being Element of Elements N st y in the carrier' of N holds
( x in Post (N,y) iff post N,y,x )
let y be Element of Elements N; ::_thesis: ( y in the carrier' of N implies ( x in Post (N,y) iff post N,y,x ) )
assume A1: y in the carrier' of N ; ::_thesis: ( x in Post (N,y) iff post N,y,x )
A2: ( post N,y,x implies x in Post (N,y) )
proof
assume  post N,y,x ; ::_thesis: x in Post (N,y)
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  x in Post (N,y) by A3, Def7; ::_thesis: verum
end;
 ( x in Post (N,y) implies post N,y,x )
proof
assume  x in Post (N,y) ; ::_thesis: post N,y,x
then  [y,x] in Flow N by Def7;
hence  post N,y,x by A1, Def5; ::_thesis: verum
end;
hence  ( x in Post (N,y) iff post N,y,x ) by A2; ::_thesis: verum
end;

definition
let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func enter (N,x) ->  set  means :Def8: :: NET_1:def 8
( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Pre (N,x) ) );
existence
 ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) )
proof
 ( not x in the carrier of N or not x in the carrier' of N ) by Th4;
hence  ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Pre (N,x) ) holds
b1 = b2 by A1, XBOOLE_0:def_3;
end;

:: deftheorem Def8 defines enter NET_1:def_8_:_
 for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = enter (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Pre (N,x) ) ) );

theorem Th15: :: NET_1:15
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
proof
let N be Pnet; ::_thesis: for x being Element of Elements N holds
( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
let x be Element of Elements N; ::_thesis: ( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
assume  Elements N <> {} ; ::_thesis: ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
then  ( x in the carrier of N or x in the carrier' of N ) by XBOOLE_0:def_3;
hence  ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) by Def8; ::_thesis: verum
end;

theorem Th16: :: NET_1:16
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N
proof
let N be Pnet; ::_thesis: for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N
let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies enter (N,x) c= Elements N )
assume A1: Elements N <> {} ; ::_thesis: enter (N,x) c= 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 set st y in {x} holds
y in Elements N by TARSKI:def_1;
assume  enter (N,x) = {x} ; ::_thesis: enter (N,x) c= Elements N
hence  enter (N,x) c= Elements N by A3, TARSKI:def_3; ::_thesis: verum
end;
 ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) by A1, Th15;
hence  enter (N,x) c= Elements N by A2, Th9; ::_thesis: verum
end;

theorem :: NET_1:17
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
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: :: NET_1:def 9
( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Post (N,x) ) );
existence
 ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) )
proof
 ( not x in the carrier of N or not x in the carrier' of N ) by Th4;
hence  ex b1 being set st
( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Post (N,x) ) holds
b1 = b2 by A1, XBOOLE_0:def_3;
end;

:: deftheorem Def9 defines exit NET_1:def_9_:_
 for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = exit (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Post (N,x) ) ) );

theorem Th18: :: NET_1:18
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )
proof
let N be Pnet; ::_thesis: for x being Element of Elements N holds
( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )
let x be Element of Elements N; ::_thesis: ( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) )
assume  Elements N <> {} ; ::_thesis: ( exit (N,x) = {x} or exit (N,x) = Post (N,x) )
then  ( x in the carrier of N or x in the carrier' of N ) by XBOOLE_0:def_3;
hence  ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by Def9; ::_thesis: verum
end;

theorem Th19: :: NET_1:19
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N
proof
let N be Pnet; ::_thesis: for x being Element of Elements N st Elements N <> {} holds
exit (N,x) c= Elements N
let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies exit (N,x) c= Elements N )
assume A1: Elements N <> {} ; ::_thesis: exit (N,x) c= 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 set st y in {x} holds
y in Elements N by TARSKI:def_1;
assume  exit (N,x) = {x} ; ::_thesis: exit (N,x) c= Elements N
hence  exit (N,x) c= Elements N by A3, TARSKI:def_3; ::_thesis: verum
end;
 ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by A1, Th18;
hence  exit (N,x) c= Elements N by A2, Th11; ::_thesis: verum
end;

theorem :: NET_1:20
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
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 :: NET_1:def 10
(enter (N,x)) \/ (exit (N,x));
correctness
coherence
(enter (N,x)) \/ (exit (N,x)) is set ;
;
end;

:: deftheorem  defines field NET_1:def_10_:_
 for N being Pnet
for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x));

definition
let N be PT_net_Str ;
let x be Element of the carrier' of N;
func Prec (N,x) ->  set  means :: NET_1:def 11
 for y being set holds
( y in it iff ( y in the carrier of N & [y,x] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) )
proof
defpred S1[ 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 & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) holds
b1 = b2
proof
let X, Y be set ; ::_thesis: ( ( for y being set holds
( y in X iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in Y iff ( y in the carrier of N & [y,x] in Flow N ) ) ) implies X = Y )
assume that
A1: for y being set holds
( y in X iff ( y in the carrier of N & [y,x] in Flow N ) ) and
A2: for y being set holds
( y in Y iff ( y in the carrier of N & [y,x] in Flow N ) ) ; ::_thesis: X = Y
A3: for y being set st y in Y holds
y in X
proof
let y be set ; ::_thesis: ( y in Y implies y in X )
assume  y in Y ; ::_thesis: y in X
then  ( y in the carrier of N & [y,x] in Flow N ) by A2;
hence  y in X by A1; ::_thesis: verum
end;
 for y being set st y in X holds
y in Y
proof
let y be set ; ::_thesis: ( y in X implies y in Y )
assume  y in X ; ::_thesis: y in Y
then  ( y in the carrier of N & [y,x] in Flow N ) by A1;
hence  y in Y by A2; ::_thesis: verum
end;
hence  X = Y by A3, TARSKI:1; ::_thesis: verum
end;
func Postc (N,x) ->  set  means :: NET_1:def 12
 for y being set holds
( y in it iff ( y in the carrier of N & [x,y] in Flow N ) );
existence
 ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) )
proof
defpred S1[ 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 & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) holds
b1 = b2
proof
let X, Y be set ; ::_thesis: ( ( for y being set holds
( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ) implies X = Y )
assume that
A4: for y being set holds
( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) and
A5: for y being set holds
( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ; ::_thesis: X = Y
A6: for y being set st y in Y holds
y in X
proof
let y be set ; ::_thesis: ( y in Y implies y in X )
assume  y in Y ; ::_thesis: y in X
then  ( y in the carrier of N & [x,y] in Flow N ) by A5;
hence  y in X by A4; ::_thesis: verum
end;
 for y being set st y in X holds
y in Y
proof
let y be set ; ::_thesis: ( y in X implies y in Y )
assume  y in X ; ::_thesis: y in Y
then  ( y in the carrier of N & [x,y] in Flow N ) by A4;
hence  y in Y by A5; ::_thesis: verum
end;
hence  X = Y by A6, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem  defines Prec NET_1:def_11_:_
 for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Prec (N,x) iff for y being set holds
( y in b3 iff ( y in the carrier of N & [y,x] in Flow N ) ) );

:: deftheorem  defines Postc NET_1:def_12_:_
 for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Postc (N,x) iff for y being set holds
( y in b3 iff ( y in the carrier of N & [x,y] in Flow N ) ) );

definition
let N be Pnet;
let X be set ;
func Entr (N,X) ->  set  means :Def13: :: NET_1:def 13
 for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
take  F ; ::_thesis: for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) )
thus  for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) holds
b1 = b2
proof
let W, Y be set ; ::_thesis: ( ( for x being set holds
( x in W iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ) implies W = Y )
assume that
A2: for x being set 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 being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) ; ::_thesis: W = Y
A4: for x being set st x in Y holds
x in W
proof
let x be set ; ::_thesis: ( x in Y implies x in W )
assume  x in Y ; ::_thesis: x in W
then  ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) by A3;
hence  x in W by A2; ::_thesis: verum
end;
 for x being set st x in W holds
x in Y
proof
let x be set ; ::_thesis: ( x in W implies x in Y )
assume  x in W ; ::_thesis: x in Y
then  ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) by A2;
hence  x in Y by A3; ::_thesis: verum
end;
hence  W = Y by A4, TARSKI:1; ::_thesis: verum
end;
func Ext (N,X) ->  set  means :Def14: :: NET_1:def 14
 for x being set holds
( x in it iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) )
proof
defpred S1[ 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 S1[x] ) from SUBSET_1:sch_3();
take  F ; ::_thesis: for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) )
thus  for x being set holds
( x in F iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) by A5; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) holds
b1 = b2
proof
let W, Y be set ; ::_thesis: ( ( for x being set holds
( x in W iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ) implies W = Y )
assume that
A6: for x being set 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 being set holds
( x in Y iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) ; ::_thesis: W = Y
A8: for x being set st x in Y holds
x in W
proof
let x be set ; ::_thesis: ( x in Y implies x in W )
assume  x in Y ; ::_thesis: x in W
then  ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) by A7;
hence  x in W by A6; ::_thesis: verum
end;
 for x being set st x in W holds
x in Y
proof
let x be set ; ::_thesis: ( x in W implies x in Y )
assume  x in W ; ::_thesis: x in Y
then  ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) by A6;
hence  x in Y by A7; ::_thesis: verum
end;
hence  W = Y by A8, TARSKI:1; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines Entr NET_1:def_13_:_
 for N being Pnet
for X being set
for b3 being set holds
( b3 = Entr (N,X) iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter (N,y) ) ) ) );

:: deftheorem Def14 defines Ext NET_1:def_14_:_
 for N being Pnet
for X being set
for b3 being set holds
( b3 = Ext (N,X) iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit (N,y) ) ) ) );

theorem Th21: :: NET_1:21
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
enter (N,x) in Entr (N,X)
proof
let N be Pnet; ::_thesis: for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
enter (N,x) in Entr (N,X)
let x be Element of Elements N; ::_thesis: for X being set st Elements N <> {} & x in X holds
enter (N,x) in Entr (N,X)
let X be set ; ::_thesis: ( Elements N <> {} & x in X implies enter (N,x) in Entr (N,X) )
assume that
A1: Elements N <> {} and
A2: x in X ; ::_thesis: enter (N,x) in Entr (N,X)
 enter (N,x) c= Elements N by A1, Th16;
hence  enter (N,x) in Entr (N,X) by A2, Def13; ::_thesis: verum
end;

theorem Th22: :: NET_1:22
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
exit (N,x) in Ext (N,X)
proof
let N be Pnet; ::_thesis: for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
exit (N,x) in Ext (N,X)
let x be Element of Elements N; ::_thesis: for X being set st Elements N <> {} & x in X holds
exit (N,x) in Ext (N,X)
let X be set ; ::_thesis: ( Elements N <> {} & x in X implies exit (N,x) in Ext (N,X) )
assume that
A1: Elements N <> {} and
A2: x in X ; ::_thesis: exit (N,x) in Ext (N,X)
 exit (N,x) c= Elements N by A1, Th19;
hence  exit (N,x) in Ext (N,X) by A2, Def14; ::_thesis: verum
end;

definition
let N be Pnet;
let X be set ;
func Input (N,X) ->  set  equals :: NET_1:def 15
 union (Entr (N,X));
correctness
coherence
union (Entr (N,X)) is set ;
;
func Output (N,X) ->  set  equals :: NET_1:def 16
 union (Ext (N,X));
correctness
coherence
union (Ext (N,X)) is set ;
;
end;

:: deftheorem  defines Input NET_1:def_15_:_
 for N being Pnet
for X being set holds Input (N,X) = union (Entr (N,X));

:: deftheorem  defines Output NET_1:def_16_:_
 for N being Pnet
for X being set holds Output (N,X) = union (Ext (N,X));

theorem :: NET_1:23
for N being Pnet
for x, X being set st X c= Elements N holds
( 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; ::_thesis: for x, X being set st X c= Elements N holds
( x in Input (N,X) iff ex y being Element of Elements N st
( y in X & x in enter (N,y) ) )
let x, X be set ; ::_thesis: ( 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) ) ) )
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) ; ::_thesis: ex y being Element of Elements N st
( y in X & x in enter (N,y) )
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  ex y being Element of Elements N st
( y in X & x in enter (N,y) ) by A2; ::_thesis: verum
end;
assume A4: X c= Elements N ; ::_thesis: ( x in Input (N,X) iff ex y being Element of Elements N st
( y in X & x in enter (N,y) ) )
 ( 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) ; ::_thesis: x in Input (N,X)
 enter (N,y) in Entr (N,X) by A4, A5, Th21;
hence  x in Input (N,X) by A6, TARSKI:def_4; ::_thesis: verum
end;
hence  ( x in Input (N,X) iff ex y being Element of Elements N st
( y in X & x in enter (N,y) ) ) by A1; ::_thesis: verum
end;

theorem :: NET_1:24
for N being Pnet
for x, X being set st X c= Elements N holds
( 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; ::_thesis: for x, X being set st X c= Elements N holds
( x in Output (N,X) iff ex y being Element of Elements N st
( y in X & x in exit (N,y) ) )
let x, X be set ; ::_thesis: ( 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) ) ) )
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) ; ::_thesis: ex y being Element of Elements N st
( y in X & x in exit (N,y) )
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  ex y being Element of Elements N st
( y in X & x in exit (N,y) ) by A2; ::_thesis: verum
end;
assume A4: X c= Elements N ; ::_thesis: ( x in Output (N,X) iff ex y being Element of Elements N st
( y in X & x in exit (N,y) ) )
 ( 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) ; ::_thesis: x in Output (N,X)
 exit (N,y) in Ext (N,X) by A4, A5, Th22;
hence  x in Output (N,X) by A6, TARSKI:def_4; ::_thesis: verum
end;
hence  ( x in Output (N,X) iff ex y being Element of Elements N st
( y in X & x in exit (N,y) ) ) by A1; ::_thesis: verum
end;

theorem :: NET_1:25
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( 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; ::_thesis: for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
let X be Subset of (Elements N); ::_thesis: for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
let x be Element of Elements N; ::_thesis: ( 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 ) ) ) )
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 ; ::_thesis: x in Input (N,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  x in Input (N,X) by A6, TARSKI:def_4; ::_thesis: verum
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 ; ::_thesis: x in Input (N,X)
 ( 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  x in Input (N,X) by A10, TARSKI:def_4; ::_thesis: verum
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 ) ) ; ::_thesis: x in Input (N,X)
hence  x in Input (N,X) by A7, A2; ::_thesis: verum
end;
assume A11: Elements N <> {} ; ::_thesis: ( 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 ) ) )
 ( not x in Input (N,X) or ( 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) ; ::_thesis: ( ( 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 ) )
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 ; ::_thesis: ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x )
take  z ; ::_thesis: ( z in X & z in the carrier' of N & pre N,z,x )
 [x,z] in Flow N by A13, A16, A18, Def6;
hence  ( z in X & z in the carrier' of N & pre N,z,x ) by A14, A18, Def4; ::_thesis: verum
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  ( ( 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 ) ) by A13, A14, A19, A17, TARSKI:def_1; ::_thesis: verum
end;
hence  ( 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 ) ) ) by A1; ::_thesis: verum
end;

theorem :: NET_1:26
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( 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; ::_thesis: for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
let X be Subset of (Elements N); ::_thesis: for x being Element of Elements N st Elements N <> {} holds
( 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 ) ) )
let x be Element of Elements N; ::_thesis: ( 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 ) ) ) )
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 ; ::_thesis: x in Output (N,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  x in Output (N,X) by A6, TARSKI:def_4; ::_thesis: verum
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 ; ::_thesis: x in Output (N,X)
 ( 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  x in Output (N,X) by A10, TARSKI:def_4; ::_thesis: verum
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 ) ) ; ::_thesis: x in Output (N,X)
hence  x in Output (N,X) by A7, A2; ::_thesis: verum
end;
assume A11: Elements N <> {} ; ::_thesis: ( 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 ) ) )
 ( not x in Output (N,X) or ( 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) ; ::_thesis: ( ( 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 ) )
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 ; ::_thesis: ex y being Element of Elements N st
( y in X & y in the carrier' of N & post N,y,x )
take  z ; ::_thesis: ( z in X & z in the carrier' of N & post N,z,x )
 [z,x] in Flow N by A13, A16, A18, Def7;
hence  ( z in X & z in the carrier' of N & post N,z,x ) by A14, A18, Def5; ::_thesis: verum
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  ( ( 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 ) ) by A13, A14, A19, A17, TARSKI:def_1; ::_thesis: verum
end;
hence  ( 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 ) ) ) by A1; ::_thesis: verum
end;