:: E_SIEC semantic presentation

begin


definition
attrc1 is strict ;
struct G_Net  ->  1-sorted ;
aggrG_Net(# carrier, entrance, escape #) ->  G_Net ;
sel entrance c1 ->  Relation;
sel escape c1 ->  Relation;
end;

definition
let IT be G_Net ;
attrIT is GG  means :Def1: :: E_SIEC:def 1
( the entrance of IT c= [: the carrier of IT, the carrier of IT:] & the escape of IT c= [: the carrier of IT, the carrier of IT:] & the entrance of IT * the entrance of IT = the entrance of IT & the entrance of IT * the escape of IT = the entrance of IT & the escape of IT * the escape of IT = the escape of IT & the escape of IT * the entrance of IT = the escape of IT );
end;

:: deftheorem Def1 defines GG E_SIEC:def_1_:_
 for IT being G_Net holds
( IT is GG iff ( the entrance of IT c= [: the carrier of IT, the carrier of IT:] & the escape of IT c= [: the carrier of IT, the carrier of IT:] & the entrance of IT * the entrance of IT = the entrance of IT & the entrance of IT * the escape of IT = the entrance of IT & the escape of IT * the escape of IT = the escape of IT & the escape of IT * the entrance of IT = the escape of IT ) );

registration
cluster GG for G_Net ;
existence
 ex b1 being G_Net st b1 is GG
proof
take N = G_Net(# {},{},{} #); ::_thesis: N is GG
 ( the escape of N c= [: the carrier of N, the carrier of N:] & the entrance of N * the entrance of N = {} ) by XBOOLE_1:2;
hence  N is GG by Def1; ::_thesis: verum
end;
end;

definition
mode gg_net is GG G_Net ;
end;

definition
let IT be G_Net ;
attrIT is EE  means :Def2: :: E_SIEC:def 2
( the entrance of IT * ( the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * ( the escape of IT \ (id the carrier of IT)) = {} );
end;

:: deftheorem Def2 defines EE E_SIEC:def_2_:_
 for IT being G_Net holds
( IT is EE iff ( the entrance of IT * ( the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * ( the escape of IT \ (id the carrier of IT)) = {} ) );

registration
cluster EE for G_Net ;
existence
 ex b1 being G_Net st b1 is EE
proof
take N = G_Net(# {},{},{} #); ::_thesis: N is EE
 the entrance of N * ( the entrance of N \ (id N)) = {} ;
hence  N is EE by Def2; ::_thesis: verum
end;
end;

registration
cluster strict GG EE for G_Net ;
existence
 ex b1 being G_Net st
( b1 is strict & b1 is GG & b1 is EE )
proof
take N = G_Net(# {},{},{} #); ::_thesis: ( N is strict & N is GG & N is EE )
 ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N * ( the escape of N \ (id N)) = {} ) by XBOOLE_1:2;
hence  ( N is strict & N is GG & N is EE ) by Def1, Def2; ::_thesis: verum
end;
end;

definition
mode e_net is GG EE G_Net ;
end;

theorem :: E_SIEC:1
for X being set
for R, S being Relation holds
( G_Net(# X,R,S #) is e_net iff ( R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ (id X)) = {} & S * (S \ (id X)) = {} ) ) by Def1, Def2;

theorem Th2: :: E_SIEC:2
for X being set holds G_Net(# X,{},{} #) is e_net
proof
let X be set ; ::_thesis: G_Net(# X,{},{} #) is e_net
 ( {} c= [:X,X:] & {} * ({} \ (id X)) = {} ) by XBOOLE_1:2;
hence  G_Net(# X,{},{} #) is e_net by Def1, Def2; ::_thesis: verum
end;

theorem Th3: :: E_SIEC:3
for X being set holds G_Net(# X,(id X),(id X) #) is e_net
proof
let X be set ; ::_thesis: G_Net(# X,(id X),(id X) #) is e_net
A1: (id X) * ((id X) \ (id X)) = (id X) * {} by XBOOLE_1:37
.= {} ;
 ( id X c= [:X,X:] & (id X) * (id X) = id X ) by RELSET_1:13, SYSREL:12;
hence  G_Net(# X,(id X),(id X) #) is e_net by A1, Def1, Def2; ::_thesis: verum
end;

theorem :: E_SIEC:4
G_Net(# {},{},{} #) is e_net by Th2;

theorem :: E_SIEC:5
for X, Y being set holds G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net
proof
let X, Y be set ; ::_thesis: G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net
A1: (id (X \ Y)) * ((id (X \ Y)) \ (id X)) = (id (X \ Y)) * {} by SYSREL:16
.= {} ;
 X \ Y c= X by XBOOLE_1:36;
then A2: [:(X \ Y),(X \ Y):] c= [:X,X:] by ZFMISC_1:96;
 id (X \ Y) c= [:(X \ Y),(X \ Y):] by RELSET_1:13;
then A3: id (X \ Y) c= [:X,X:] by A2, XBOOLE_1:1;
 (id (X \ Y)) * (id (X \ Y)) = id (X \ Y) by SYSREL:12;
hence  G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net by A3, A1, Def1, Def2; ::_thesis: verum
end;

definition
func empty_e_net  ->  strict e_net equals :: E_SIEC:def 3
 G_Net(# {},{},{} #);
correctness
coherence
G_Net(# {},{},{} #) is strict e_net;
by Th2;
end;

:: deftheorem  defines empty_e_net E_SIEC:def_3_:_
 empty_e_net = G_Net(# {},{},{} #);

definition
let X be set ;
func Tempty_e_net X ->  strict e_net equals :: E_SIEC:def 4
 G_Net(# X,(id X),(id X) #);
coherence
 G_Net(# X,(id X),(id X) #) is strict e_net by Th3;
func Pempty_e_net X ->  strict e_net equals :: E_SIEC:def 5
 G_Net(# X,{},{} #);
coherence
 G_Net(# X,{},{} #) is strict e_net by Th2;
end;

:: deftheorem  defines Tempty_e_net E_SIEC:def_4_:_
 for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #);

:: deftheorem  defines Pempty_e_net E_SIEC:def_5_:_
 for X being set holds Pempty_e_net X = G_Net(# X,{},{} #);

theorem :: E_SIEC:6
for X being set holds
( the carrier of (Tempty_e_net X) = X & the entrance of (Tempty_e_net X) = id X & the escape of (Tempty_e_net X) = id X ) ;

theorem :: E_SIEC:7
for X being set holds
( the carrier of (Pempty_e_net X) = X & the entrance of (Pempty_e_net X) = {} & the escape of (Pempty_e_net X) = {} ) ;

definition
let x be set ;
func Psingle_e_net x ->  strict e_net equals :: E_SIEC:def 6
 G_Net(# {x},(id {x}),(id {x}) #);
coherence
 G_Net(# {x},(id {x}),(id {x}) #) is strict e_net by Th3;
func Tsingle_e_net x ->  strict e_net equals :: E_SIEC:def 7
 G_Net(# {x},{},{} #);
coherence
 G_Net(# {x},{},{} #) is strict e_net by Th2;
end;

:: deftheorem  defines Psingle_e_net E_SIEC:def_6_:_
 for x being set holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);

:: deftheorem  defines Tsingle_e_net E_SIEC:def_7_:_
 for x being set holds Tsingle_e_net x = G_Net(# {x},{},{} #);

theorem :: E_SIEC:8
for x being set holds
( the carrier of (Psingle_e_net x) = {x} & the entrance of (Psingle_e_net x) = id {x} & the escape of (Psingle_e_net x) = id {x} ) ;

theorem :: E_SIEC:9
for x being set holds
( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;

theorem Th10: :: E_SIEC:10
for X, Y being set holds G_Net(# (X \/ Y),(id X),(id X) #) is e_net
proof
let X, Y be set ; ::_thesis: G_Net(# (X \/ Y),(id X),(id X) #) is e_net
 X c= X \/ Y by XBOOLE_1:7;
then  ( id X c= [:X,X:] & [:X,X:] c= [:(X \/ Y),(X \/ Y):] ) by RELSET_1:13, ZFMISC_1:96;
then A1: id X c= [:(X \/ Y),(X \/ Y):] by XBOOLE_1:1;
 id X c= (id X) \/ (id Y) by XBOOLE_1:7;
then  id X c= id (X \/ Y) by SYSREL:14;
then A2: (id X) * ((id X) \ (id (X \/ Y))) = (id X) * {} by XBOOLE_1:37
.= {} ;
 (id X) * (id X) = id X by SYSREL:12;
hence  G_Net(# (X \/ Y),(id X),(id X) #) is e_net by A1, A2, Def1, Def2; ::_thesis: verum
end;

definition
let X, Y be set ;
func PTempty_e_net (X,Y) ->  strict e_net equals :: E_SIEC:def 8
 G_Net(# (X \/ Y),(id X),(id X) #);
coherence
 G_Net(# (X \/ Y),(id X),(id X) #) is strict e_net by Th10;
end;

:: deftheorem  defines PTempty_e_net E_SIEC:def_8_:_
 for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #);

theorem Th11: :: E_SIEC:11
for N being e_net holds
( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) )
proof
let N be e_net; ::_thesis: ( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) )
 ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N c= [: the carrier of N, the carrier of N:] ) by Def1;
hence  ( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) ) by SYSREL:20; ::_thesis: verum
end;

theorem Th12: :: E_SIEC:12
for N being e_net holds CL the entrance of N = CL the escape of N
proof
let N be e_net; ::_thesis: CL the entrance of N = CL the escape of N
 the escape of N * ( the escape of N \ (id N)) = {} by Def2;
then A1: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;
 the entrance of N * ( the entrance of N \ (id N)) = {} by Def2;
then A2: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;
 ( the entrance of N * the escape of N = the entrance of N & the escape of N * the entrance of N = the escape of N ) by Def1;
hence  CL the entrance of N = CL the escape of N by A1, A2, SYSREL:40; ::_thesis: verum
end;

theorem Th13: :: E_SIEC:13
for N being e_net holds
( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N )
proof
let N be e_net; ::_thesis: ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N )
 the entrance of N * ( the entrance of N \ (id the carrier of N)) = {} by Def2;
then A1: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;
 the escape of N * ( the escape of N \ (id the carrier of N)) = {} by Def2;
then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;
A3: the escape of N * the escape of N = the escape of N by Def1;
then A4: rng the escape of N = rng (CL the escape of N) by A2, SYSREL:31;
A5: the entrance of N * the entrance of N = the entrance of N by Def1;
then  rng the entrance of N = rng (CL the entrance of N) by A1, SYSREL:31;
hence  ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N ) by A5, A1, A3, A2, A4, Th12, SYSREL:31; ::_thesis: verum
end;

theorem Th14: :: E_SIEC:14
for N being e_net holds
( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N )
proof
let N be e_net; ::_thesis: ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N )
 ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N c= [: the carrier of N, the carrier of N:] ) by Def1;
hence  ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N ) by SYSREL:3; ::_thesis: verum
end;

theorem Th15: :: E_SIEC:15
for N being e_net holds
( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} )
proof
let N be e_net; ::_thesis: ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} )
set R = the entrance of N;
set S = the escape of N;
set T = id the carrier of N;
A1: the escape of N * ( the entrance of N \ (id the carrier of N)) = the escape of N * ( the entrance of N \ (id (dom the entrance of N))) by Th11
.= ( the escape of N * the entrance of N) * ( the entrance of N \ (id (dom the entrance of N))) by Def1
.= the escape of N * ( the entrance of N * ( the entrance of N \ (id (dom the entrance of N)))) by RELAT_1:36
.= the escape of N * ( the entrance of N * ( the entrance of N \ (id the carrier of N))) by Th11
.= the escape of N * {} by Def2
.= {} ;
the entrance of N * ( the escape of N \ (id the carrier of N)) = the entrance of N * ( the escape of N \ (id (dom the escape of N))) by Th11
.= ( the entrance of N * the escape of N) * ( the escape of N \ (id (dom the escape of N))) by Def1
.= the entrance of N * ( the escape of N * ( the escape of N \ (id (dom the escape of N)))) by RELAT_1:36
.= the entrance of N * ( the escape of N * ( the escape of N \ (id the carrier of N))) by Th11
.= the entrance of N * {} by Def2
.= {} ;
hence  ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} ) by A1; ::_thesis: verum
end;

theorem :: E_SIEC:16
for N being e_net holds
( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} )
proof
let N be e_net; ::_thesis: ( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} )
set R = the entrance of N;
set S = the escape of N;
set T = id the carrier of N;
 ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A1: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;
 ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A2: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;
 ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A3: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15;
 ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;
hence  ( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; ::_thesis: verum
end;

definition
let N be e_net;
func e_Places N ->  set  equals :: E_SIEC:def 9
 rng the entrance of N;
correctness
coherence
rng the entrance of N is set ;
;
end;

:: deftheorem  defines e_Places E_SIEC:def_9_:_
 for N being e_net holds e_Places N = rng the entrance of N;

definition
let N be e_net;
func e_Transitions N ->  set  equals :: E_SIEC:def 10
 the carrier of N \ (e_Places N);
correctness
coherence
the carrier of N \ (e_Places N) is set ;
;
end;

:: deftheorem  defines e_Transitions E_SIEC:def_10_:_
 for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);

theorem Th17: :: E_SIEC:17
for x, y being set
for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds
( x in e_Transitions N & y in e_Places N )
proof
let x, y be set ; ::_thesis: for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds
( x in e_Transitions N & y in e_Places N )
let N be e_net; ::_thesis: ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
A1: ( [x,y] in the escape of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
proof
 the escape of N * ( the escape of N \ (id the carrier of N)) = {} by Def2;
then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11;
 dom the escape of N c= the carrier of N by Th14;
then A3: (dom the escape of N) \ (dom (CL the escape of N)) c= the carrier of N \ (dom (CL the escape of N)) by XBOOLE_1:33;
assume A4: ( [x,y] in the escape of N & x <> y ) ; ::_thesis: ( x in e_Transitions N & y in e_Places N )
A5: the escape of N * the escape of N = the escape of N by Def1;
then  x in (dom the escape of N) \ (dom (CL the escape of N)) by A4, A2, SYSREL:30;
then  x in the carrier of N \ (dom (CL the escape of N)) by A3;
then A6: x in the carrier of N \ (rng the escape of N) by Th13;
 y in dom (CL the escape of N) by A4, A5, A2, SYSREL:30;
then  y in rng the escape of N by Th13;
hence  ( x in e_Transitions N & y in e_Places N ) by A6, Th13; ::_thesis: verum
end;
 ( [x,y] in the entrance of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) )
proof
 the entrance of N * ( the entrance of N \ (id the carrier of N)) = {} by Def2;
then A7: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11;
 dom the entrance of N c= the carrier of N by Th14;
then A8: (dom the entrance of N) \ (dom (CL the entrance of N)) c= the carrier of N \ (dom (CL the entrance of N)) by XBOOLE_1:33;
assume A9: ( [x,y] in the entrance of N & x <> y ) ; ::_thesis: ( x in e_Transitions N & y in e_Places N )
A10: the entrance of N * the entrance of N = the entrance of N by Def1;
then  x in (dom the entrance of N) \ (dom (CL the entrance of N)) by A9, A7, SYSREL:30;
then A11: x in the carrier of N \ (dom (CL the entrance of N)) by A8;
 y in dom (CL the entrance of N) by A9, A10, A7, SYSREL:30;
hence  ( x in e_Transitions N & y in e_Places N ) by A11, Th13; ::_thesis: verum
end;
hence  ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) ) by A1; ::_thesis: verum
end;

theorem Th18: :: E_SIEC:18
for N being e_net holds
( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )
proof
let N be e_net; ::_thesis: ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )
A1: for x, y being set st [x,y] in the entrance of N \ (id the carrier of N) holds
[x,y] in [:(e_Transitions N),(e_Places N):]
proof
let x, y be set ; ::_thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] )
assume A2: [x,y] in the entrance of N \ (id the carrier of N) ; ::_thesis: [x,y] in [:(e_Transitions N),(e_Places N):]
then  [x,y] in the entrance of N by XBOOLE_0:def_5;
then A3: x in dom the entrance of N by XTUPLE_0:def_12;
 not [x,y] in id the carrier of N by A2, XBOOLE_0:def_5;
then A4: ( not x in the carrier of N or x <> y ) by RELAT_1:def_10;
A5: [x,y] in the entrance of N by A2, XBOOLE_0:def_5;
then A6: y in e_Places N by XTUPLE_0:def_13;
 dom the entrance of N c= the carrier of N by Th14;
then  x in e_Transitions N by A5, A4, A3, Th17;
hence  [x,y] in [:(e_Transitions N),(e_Places N):] by A6, ZFMISC_1:87; ::_thesis: verum
end;
 for x, y being set st [x,y] in the escape of N \ (id the carrier of N) holds
[x,y] in [:(e_Transitions N),(e_Places N):]
proof
let x, y be set ; ::_thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] )
A7: dom the escape of N c= the carrier of N by Th14;
assume A8: [x,y] in the escape of N \ (id the carrier of N) ; ::_thesis: [x,y] in [:(e_Transitions N),(e_Places N):]
then  [x,y] in the escape of N by XBOOLE_0:def_5;
then A9: x in dom the escape of N by XTUPLE_0:def_12;
 not [x,y] in id the carrier of N by A8, XBOOLE_0:def_5;
then A10: ( not x in the carrier of N or x <> y ) by RELAT_1:def_10;
 [x,y] in the escape of N by A8, XBOOLE_0:def_5;
then  ( x in e_Transitions N & y in e_Places N ) by A10, A9, A7, Th17;
hence  [x,y] in [:(e_Transitions N),(e_Places N):] by ZFMISC_1:87; ::_thesis: verum
end;
hence  ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by A1, RELAT_1:def_3; ::_thesis: verum
end;

definition
let N be e_net;
func e_Flow N ->  Relation equals :: E_SIEC:def 11
(( the entrance of N ~) \/ the escape of N) \ (id N);
correctness
coherence
(( the entrance of N ~) \/ the escape of N) \ (id N) is Relation;
;
end;

:: deftheorem  defines e_Flow E_SIEC:def_11_:_
 for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N);

theorem :: E_SIEC:19
for N being e_net holds e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):]
proof
let N be e_net; ::_thesis: e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):]
A1: ( the entrance of N ~) \ (id N) = ( the entrance of N ~) \ ((id the carrier of N) ~) by RELAT_1:46
.= ( the entrance of N \ (id the carrier of N)) ~ by RELAT_1:24 ;
A2: ( e_Flow N = (( the entrance of N ~) \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)) & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th18, XBOOLE_1:42;
 the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] by Th18;
then  ( the entrance of N ~) \ (id the carrier of N) c= [:(e_Places N),(e_Transitions N):] by A1, SYSREL:4;
hence  e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] by A2, XBOOLE_1:13; ::_thesis: verum
end;

definition
let N be e_net;
func e_pre N ->  Relation equals :: E_SIEC:def 12
 the entrance of N \ (id the carrier of N);
correctness
coherence
the entrance of N \ (id the carrier of N) is Relation;
;
func e_post N ->  Relation equals :: E_SIEC:def 13
 the escape of N \ (id the carrier of N);
correctness
coherence
the escape of N \ (id the carrier of N) is Relation;
;
end;

:: deftheorem  defines e_pre E_SIEC:def_12_:_
 for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N);

:: deftheorem  defines e_post E_SIEC:def_13_:_
 for N being e_net holds e_post N = the escape of N \ (id the carrier of N);

theorem :: E_SIEC:20
for N being e_net holds
( e_pre N c= [:(e_Transitions N),(e_Places N):] & e_post N c= [:(e_Transitions N),(e_Places N):] ) by Th18;

definition
let N be e_net;
func e_shore N ->  set  equals :: E_SIEC:def 14
 the carrier of N;
correctness
coherence
the carrier of N is set ;
;
func e_prox N ->  Relation equals :: E_SIEC:def 15
( the entrance of N \/ the escape of N) ~ ;
correctness
coherence
( the entrance of N \/ the escape of N) ~ is Relation;
;
func e_flow N ->  Relation equals :: E_SIEC:def 16
(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);
correctness
coherence
(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N) is Relation;
;
end;

:: deftheorem  defines e_shore E_SIEC:def_14_:_
 for N being e_net holds e_shore N = the carrier of N;

:: deftheorem  defines e_prox E_SIEC:def_15_:_
 for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ;

:: deftheorem  defines e_flow E_SIEC:def_16_:_
 for N being e_net holds e_flow N = (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

theorem :: E_SIEC:21
for N being e_net holds
( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
proof
let N be e_net; ::_thesis: ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
A1: id the carrier of N c= [: the carrier of N, the carrier of N:] by RELSET_1:13;
A2: the escape of N c= [: the carrier of N, the carrier of N:] by Def1;
A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1;
then  the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4;
then A4: ( the entrance of N ~) \/ the escape of N c= [: the carrier of N, the carrier of N:] by A2, XBOOLE_1:8;
 the entrance of N \/ the escape of N c= [: the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1:8;
hence  ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) by A4, A1, SYSREL:4, XBOOLE_1:8; ::_thesis: verum
end;

theorem :: E_SIEC:22
for N being e_net holds
( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
proof
let N be e_net; ::_thesis: ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
set R = the entrance of N;
set S = the escape of N;
set T = id the carrier of N;
A1: ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = ((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the escape of N \/ the entrance of N)) \/ (id the carrier of N) by RELAT_1:23
.= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ the escape of N) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ (( the escape of N ~) \/ the escape of N)) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4
.= (( the entrance of N ~) \/ (( the escape of N \/ ( the escape of N ~)) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= (( the entrance of N ~) \/ ( the escape of N \/ (( the escape of N ~) \/ the entrance of N))) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ the escape of N) \/ (( the escape of N ~) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= (e_flow N) \/ ((( the escape of N ~) \/ (( the entrance of N ~) ~)) \/ (id the carrier of N)) by XBOOLE_1:5
.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ (id the carrier of N)) by RELAT_1:23
.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~))
.= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ;
A2: ((e_prox N) \ (id the carrier of N)) * (e_prox N) = ((( the entrance of N ~) \/ ( the escape of N ~)) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) ~) by RELAT_1:23
.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) ~) by XBOOLE_1:42
.= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N ~) \/ ( the escape of N ~)) by RELAT_1:23
.= (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the entrance of N ~)) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by RELAT_1:32
.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by SYSREL:6
.= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) by SYSREL:6
.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~)))
.= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)))
.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24
.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24
.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24
.= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:24
.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35
.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35
.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35
.= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by RELAT_1:35
.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by Def2
.= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Def2
.= (({} ~) \/ ({} ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Th15
.= {} by Th15 ;
(e_prox N) * (e_prox N) = (( the entrance of N \/ the escape of N) * ( the entrance of N \/ the escape of N)) ~ by RELAT_1:35
.= ((( the entrance of N \/ the escape of N) * the entrance of N) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by RELAT_1:32
.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by SYSREL:6
.= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by SYSREL:6
.= (( the entrance of N \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1
.= (( the entrance of N \/ the escape of N) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1
.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N * the escape of N))) ~ by Def1
.= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ the escape of N)) ~ by Def1
.= e_prox N ;
hence  ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A2, A1; ::_thesis: verum
end;

theorem Th23: :: E_SIEC:23
for N being e_net holds
( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) )
proof
let N be e_net; ::_thesis: ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) )
set T = the entrance of N;
set C = the carrier of N;
set E = the escape of N;
set I = id the carrier of N;
 for x, y being set st [x,y] in the escape of N \ (id the carrier of N) holds
[x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))
proof
let x, y be set ; ::_thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) )
assume A1: [x,y] in the escape of N \ (id the carrier of N) ; ::_thesis: [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))
then  [x,y] in the escape of N by XBOOLE_0:def_5;
then A2: x in dom the escape of N by XTUPLE_0:def_12;
A3: not x in rng the escape of N
proof
assume  x in rng the escape of N ; ::_thesis: contradiction
then  ex z being set st [z,x] in the escape of N by XTUPLE_0:def_13;
then  the escape of N * ( the escape of N \ (id the carrier of N)) <> {} by A1, RELAT_1:def_8;
hence  contradiction by Def2; ::_thesis: verum
end;
 dom the escape of N c= the carrier of N by Th14;
then  x in the carrier of N \ (rng the escape of N) by A2, A3, XBOOLE_0:def_5;
then  [x,x] in id ( the carrier of N \ (rng the escape of N)) by RELAT_1:def_10;
hence  [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) by A1, RELAT_1:def_8; ::_thesis: verum
end;
then A4: the escape of N \ (id the carrier of N) c= (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) by RELAT_1:def_3;
 for x, y being set st [x,y] in the entrance of N \ (id the carrier of N) holds
[x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))
proof
let x, y be set ; ::_thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) )
assume A5: [x,y] in the entrance of N \ (id the carrier of N) ; ::_thesis: [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))
then  [x,y] in the entrance of N by XBOOLE_0:def_5;
then A6: x in dom the entrance of N by XTUPLE_0:def_12;
A7: not x in rng the entrance of N
proof
assume  x in rng the entrance of N ; ::_thesis: contradiction
then  ex z being set st [z,x] in the entrance of N by XTUPLE_0:def_13;
then  the entrance of N * ( the entrance of N \ (id the carrier of N)) <> {} by A5, RELAT_1:def_8;
hence  contradiction by Def2; ::_thesis: verum
end;
 dom the entrance of N c= the carrier of N by Th14;
then  x in the carrier of N \ (rng the entrance of N) by A6, A7, XBOOLE_0:def_5;
then  [x,x] in id ( the carrier of N \ (rng the entrance of N)) by RELAT_1:def_10;
hence  [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) by A5, RELAT_1:def_8; ::_thesis: verum
end;
then A8: the entrance of N \ (id the carrier of N) c= (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) by RELAT_1:def_3;
 ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) c= the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N \ (id the carrier of N) ) by RELAT_1:50;
hence  ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) ) by A4, A8, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th24: :: E_SIEC:24
for N being e_net holds
( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} )
proof
let N be e_net; ::_thesis: ( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} )
set T = the entrance of N;
set C = the carrier of N;
set E = the escape of N;
set I = id the carrier of N;
 ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A1: ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;
 ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A2: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15;
 ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then A3: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;
 ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;
hence  ( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; ::_thesis: verum
end;

theorem Th25: :: E_SIEC:25
for N being e_net holds
( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
proof
let N be e_net; ::_thesis: ( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
A1: (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = (( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~ by RELAT_1:35
.= {} by Th24, RELAT_1:43 ;
(( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = (( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~ by RELAT_1:35
.= {} by Th24, RELAT_1:43 ;
hence  ( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; ::_thesis: verum
end;

theorem :: E_SIEC:26
for N being e_net holds
( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ )
proof
let N be e_net; ::_thesis: ( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ )
A1: (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~ by RELAT_1:35
.= ( the entrance of N \ (id the carrier of N)) ~ by Th23 ;
(( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~ by RELAT_1:35
.= ( the escape of N \ (id the carrier of N)) ~ by Th23 ;
hence  ( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ ) by A1; ::_thesis: verum
end;

theorem Th27: :: E_SIEC:27
for N being e_net holds
( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} )
proof
let N be e_net; ::_thesis: ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} )
A1: for x, y being set holds not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))
proof
let x, y be set ; ::_thesis: not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))
assume  [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) ; ::_thesis: contradiction
then consider z being set  such that
A2: [x,z] in the entrance of N \ (id the carrier of N) and
A3: [z,y] in id ( the carrier of N \ (rng the entrance of N)) by RELAT_1:def_8;
 z in the carrier of N \ (rng the entrance of N) by A3, RELAT_1:def_10;
then A4: not z in rng the entrance of N by XBOOLE_0:def_5;
 [x,z] in the entrance of N by A2, XBOOLE_0:def_5;
hence  contradiction by A4, XTUPLE_0:def_13; ::_thesis: verum
end;
 for x, y being set holds not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))
proof
let x, y be set ; ::_thesis: not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))
assume  [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) ; ::_thesis: contradiction
then consider z being set  such that
A5: [x,z] in the escape of N \ (id the carrier of N) and
A6: [z,y] in id ( the carrier of N \ (rng the escape of N)) by RELAT_1:def_8;
 z in the carrier of N \ (rng the escape of N) by A6, RELAT_1:def_10;
then A7: not z in rng the escape of N by XBOOLE_0:def_5;
 [x,z] in the escape of N by A5, XBOOLE_0:def_5;
hence  contradiction by A7, XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} ) by A1, RELAT_1:37; ::_thesis: verum
end;

theorem Th28: :: E_SIEC:28
for N being e_net holds
( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
proof
let N be e_net; ::_thesis: ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} )
A1: (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)
.= (( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~ by RELAT_1:35
.= {} by Th27, RELAT_1:43 ;
(id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)
.= (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~ by RELAT_1:35
.= {} by Th27, RELAT_1:43 ;
hence  ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; ::_thesis: verum
end;

definition
let N be e_net;
func e_entrance N ->  Relation equals :: E_SIEC:def 17
(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));
correctness
coherence
(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))) is Relation;
;
func e_escape N ->  Relation equals :: E_SIEC:def 18
(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));
correctness
coherence
(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;
;
end;

:: deftheorem  defines e_entrance E_SIEC:def_17_:_
 for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

:: deftheorem  defines e_escape E_SIEC:def_18_:_
 for N being e_net holds e_escape N = (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:29
for N being e_net holds
( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N )
proof
let N be e_net; ::_thesis: ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N )
set P = the escape of N \ (id the carrier of N);
set Q = the entrance of N \ (id the carrier of N);
set S = id ( the carrier of N \ (rng the entrance of N));
set T = id ( the carrier of N \ (rng the escape of N));
A1: (e_entrance N) * (e_entrance N) = ((( the escape of N \ (id the carrier of N)) ~) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by SYSREL:6
.= (((( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32
.= (((( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:35
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N)))))
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N)))))
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by SYSREL:12
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35
.= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35
.= (({} ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th24
.= (({} ~) \/ (( the escape of N \ (id the carrier of N)) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th23
.= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27
.= e_entrance N ;
A2: (e_escape N) * (e_escape N) = ((( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6
.= (((( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:35
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N)))))
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N)))))
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35
.= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35
.= (({} ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th24
.= (({} ~) \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th23
.= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= e_escape N ;
A3: (e_escape N) * (e_entrance N) = ((( the entrance of N \ (id the carrier of N)) ~) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by SYSREL:6
.= (((( the entrance of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32
.= (((( the entrance of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:35
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N)))))
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N)))))
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by Th13
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13
.= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13
.= (({} ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th24
.= (({} ~) \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th23
.= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= e_escape N ;
(e_entrance N) * (e_escape N) = ((( the escape of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6
.= (((( the escape of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the escape of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:35
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N)))))
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N)))))
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by Th13
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by SYSREL:12
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th13
.= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th13
.= (({} ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th24
.= (({} ~) \/ (( the escape of N \ (id the carrier of N)) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th23
.= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27
.= e_entrance N ;
hence  ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N ) by A1, A3, A2; ::_thesis: verum
end;

theorem :: E_SIEC:30
for N being e_net holds
( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
proof
let N be e_net; ::_thesis: ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )
set P = the escape of N \ (id N);
set Q = the entrance of N \ (id the carrier of N);
set S = id ( the carrier of N \ (rng the entrance of N));
set T = id ( the carrier of N \ (rng the escape of N));
set R = id the carrier of N;
A1: id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
 (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) by RELAT_1:29, XBOOLE_1:36;
then  (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= {} by Th25;
then A2: (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3;
 (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) by RELAT_1:29, XBOOLE_1:36;
then  (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= {} by Th28;
then A3: (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3;
A4: (e_escape N) * ((e_escape N) \ (id (e_shore N))) = ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) * (((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) by XBOOLE_1:42
.= ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) * (((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) \/ {}) by A1, XBOOLE_1:37
.= {} \/ {} by A2, A3, SYSREL:6
.= {} ;
A5: id ( the carrier of N \ (rng the escape of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
 (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id N)) ~) by RELAT_1:29, XBOOLE_1:36;
then  (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= {} by Th28;
then A6: (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3;
 (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= (( the escape of N \ (id N)) ~) * (( the escape of N \ (id N)) ~) by RELAT_1:29, XBOOLE_1:36;
then  (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= {} by Th25;
then A7: (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3;
(e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = ((( the escape of N \ (id N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) * (((( the escape of N \ (id N)) ~) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the escape of N))) \ (id the carrier of N))) by XBOOLE_1:42
.= ((( the escape of N \ (id N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) * (((( the escape of N \ (id N)) ~) \ (id the carrier of N)) \/ {}) by A5, XBOOLE_1:37
.= {} \/ {} by A7, A6, SYSREL:6
.= {} ;
hence  ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} ) by A4; ::_thesis: verum
end;

definition
let N be e_net;
func e_adjac N ->  Relation equals :: E_SIEC:def 19
(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));
correctness
coherence
(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;
;
end;

:: deftheorem  defines e_adjac E_SIEC:def_19_:_
 for N being e_net holds e_adjac N = (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:31
for N being e_net holds
( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
proof
let N be e_net; ::_thesis: ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )
A1: ( the entrance of N \/ the escape of N) \ (id the carrier of N) c= the entrance of N \/ the escape of N by XBOOLE_1:36;
A2: the escape of N c= [: the carrier of N, the carrier of N:] by Def1;
A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1;
then  the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4;
then A4: ( id the carrier of N c= [: the carrier of N, the carrier of N:] & ( the entrance of N ~) \/ the escape of N c= [: the carrier of N, the carrier of N:] ) by A2, RELSET_1:13, XBOOLE_1:8;
 ( id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N & id the carrier of N c= [: the carrier of N, the carrier of N:] ) by RELSET_1:13, SYSREL:15, XBOOLE_1:36;
then A5: id ( the carrier of N \ (rng the entrance of N)) c= [: the carrier of N, the carrier of N:] by XBOOLE_1:1;
 the entrance of N \/ the escape of N c= [: the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1:8;
then  ( the entrance of N \/ the escape of N) \ (id the carrier of N) c= [: the carrier of N, the carrier of N:] by A1, XBOOLE_1:1;
hence  ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) by A5, A4, XBOOLE_1:8; ::_thesis: verum
end;

theorem :: E_SIEC:32
for N being e_net holds
( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
proof
let N be e_net; ::_thesis: ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )
set P = the entrance of N;
set Q = the escape of N;
set R = id the carrier of N;
set S = id ( the carrier of N \ (rng the entrance of N));
set T = id ( the carrier of N \ (rng the escape of N));
A1: id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
(e_adjac N) \/ ((e_adjac N) ~) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~) \/ ((id ( the carrier of N \ (rng the entrance of N))) ~)) by RELAT_1:23
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:5
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) ~) \ ((id the carrier of N) ~))) \/ (id ( the carrier of N \ (rng the entrance of N))) by RELAT_1:24
.= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) ~) \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))
.= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42 ;
then A2: ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \/ (id the carrier of N)) by XBOOLE_1:4
.= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id the carrier of N) by A1, XBOOLE_1:12
.= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the entrance of N \/ the escape of N)) \ (id the carrier of N)) \/ (id the carrier of N) by RELAT_1:23
.= ((( the entrance of N ~) \/ (( the escape of N \/ the entrance of N) \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ ( the escape of N \/ ( the entrance of N \/ ( the escape of N ~)))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= (((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4
.= ((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \/ (id the carrier of N) by XBOOLE_1:39
.= (e_flow N) \/ (((( the entrance of N \/ ( the escape of N ~)) ~) ~) \/ (id the carrier of N)) by XBOOLE_1:5
.= (e_flow N) \/ (((( the entrance of N ~) \/ (( the escape of N ~) ~)) ~) \/ (id the carrier of N)) by RELAT_1:23
.= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~))
.= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ;
 id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36;
then A3: (id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N) = {} by XBOOLE_1:37;
 ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15;
then A4: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
 ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2;
then A5: ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
 ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15;
then A6: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
 ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36;
then  ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2;
then A7: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3;
A8: ((e_adjac N) \ (id the carrier of N)) * (e_adjac N) = ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= (((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6
.= ((({} \/ {}) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A5, A6, SYSREL:6
.= (({} * ( the entrance of N \ (id the carrier of N))) \/ ({} * ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A3, A4, A7, SYSREL:6
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42
.= ((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41
.= ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41
.= (( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A3, SYSREL:6
.= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) by Th13
.= {} by Th27 ;
(e_adjac N) * (e_adjac N) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6
.= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42
.= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42
.= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32
.= ((({} \/ {}) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by A5, A6, SYSREL:6
.= ({} \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by A4, A7, SYSREL:6
.= ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12
.= ((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6
.= ((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32
.= ({} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13
.= {} \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27
.= (( the entrance of N \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th23
.= (( the entrance of N \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th13
.= (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th23
.= e_adjac N by XBOOLE_1:42 ;
hence  ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A8, A2; ::_thesis: verum
end;

theorem Th33: :: E_SIEC:33
for N being e_net holds
( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] )
proof
let N be e_net; ::_thesis: ( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] )
 ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th18;
hence  ( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] ) by SYSREL:4; ::_thesis: verum
end;

definition
let N be G_Net ;
func s_pre N ->  Relation equals :: E_SIEC:def 20
( the escape of N \ (id the carrier of N)) ~ ;
coherence
 ( the escape of N \ (id the carrier of N)) ~ is Relation ;
func s_post N ->  Relation equals :: E_SIEC:def 21
( the entrance of N \ (id the carrier of N)) ~ ;
coherence
 ( the entrance of N \ (id the carrier of N)) ~ is Relation ;
end;

:: deftheorem  defines s_pre E_SIEC:def_20_:_
 for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ;

:: deftheorem  defines s_post E_SIEC:def_21_:_
 for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;

theorem :: E_SIEC:34
for N being e_net holds
( s_post N c= [:(e_Places N),(e_Transitions N):] & s_pre N c= [:(e_Places N),(e_Transitions N):] ) by Th33;