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

environ

 vocabularies STRUCT_0, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, SYSREL, E_SIEC;
 notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0;
 constructors SYSREL, STRUCT_0, XTUPLE_0;
 registrations XBOOLE_0, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions STRUCT_0;
 theorems ZFMISC_1, RELAT_1, SYSREL, RELSET_1, XBOOLE_0, XBOOLE_1,XTUPLE_0;

begin

reserve x,y,z,X,Y for set;

definition
  struct (1-sorted) G_Net (# carrier -> set, entrance, escape -> Relation #);
end;

definition
  let IT be G_Net;

  attr IT is GG means :Def1:
  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;

registration
  cluster GG for G_Net;
  existence
  proof
    take N = G_Net (# {}, {}, {} #);
    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 thesis by Def1;
  end;
end;

definition
  mode gg_net is GG G_Net;
end;

definition
  let IT be G_Net;
  attr IT is EE means
  :Def2:
  (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;

registration
  cluster EE for G_Net;
  existence
  proof
    take N = G_Net (# {}, {}, {} #);
    (the entrance of N) * ((the entrance of N) \ id N) = {};
    hence thesis by Def2;
  end;
end;

registration
  cluster strict GG EE for G_Net;
  existence
  proof
    take N = G_Net (# {} , {} , {} #);
    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 thesis by Def1,Def2;
  end;
end;

definition
  mode e_net is EE GG G_Net;
end;

reserve N for e_net;

theorem
  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:
  G_Net (# X, {}, {} #) is e_net
proof
  {} c= [:X, X:] & {} * ({} \ id(X)) = {} by XBOOLE_1:2;
  hence thesis by Def1,Def2;
end;

theorem Th3:
  G_Net (# X, id X, id X #) is e_net
proof
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 thesis by A1,Def1,Def2;
end;

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

theorem
  G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net
proof
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 thesis by A3,A1,Def1,Def2;
end;

definition
  func empty_e_net -> strict e_net equals
  G_Net (# {}, {}, {} #);
  correctness by Th2;
end;

definition
  let X;
  func Tempty_e_net X -> strict e_net equals
  G_Net (# X, id X, id X #);
  coherence by Th3;
  func Pempty_e_net(X) -> strict e_net equals
  G_Net (# X, {}, {} #);
  coherence by Th2;
end;

theorem
  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
  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;
  func Psingle_e_net(x) -> strict e_net equals
  G_Net (#{x}, id{x}, id{x}#);
  coherence by Th3;
  func Tsingle_e_net(x) -> strict e_net equals
  G_Net (# {x}, {}, {} #);
  coherence by Th2;
end;

theorem
  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
  the carrier of Tsingle_e_net(x) = {x} &
  the entrance of Tsingle_e_net(x) = {} &
  the escape of Tsingle_e_net(x) = {};

theorem Th10:
  G_Net (# X \/ Y, id X, id X #) is e_net
proof
  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 thesis by A1,A2,Def1,Def2;
end;

definition
  let X,Y;
  func PTempty_e_net(X,Y) -> strict e_net equals
  G_Net (#X \/ Y, id(X), id(X)#);
  coherence by Th10;
end;

theorem Th11:
  (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
  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 thesis by SYSREL:20;
end;

theorem Th12:
  CL the entrance of N = CL the escape of N
proof
  (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 thesis by A1,A2,SYSREL:40;
end;

theorem Th13:
  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
  (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 thesis by A5,A1,A3,A2,A4,Th12,SYSREL:31;
end;

theorem Th14:
  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
  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 thesis by SYSREL:3;
end;

theorem Th15:
  (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
  set R = the entrance of N;
  set S = the escape of N;
  set T = id the carrier of N;
A1: S * (R \ T) = S * (R \ id dom R) by Th11
    .= (S * R) * (R \ id dom R) by Def1
    .= S * (R * (R \ id dom R)) by RELAT_1:36
    .= S * (R * (R \ T)) by Th11
    .= S * {} by Def2
    .= {};
  R * (S \ T) = R * (S \ id dom S) by Th11
    .= (R * S) * (S \ id dom S) by Def1
    .= R * (S * (S \ id dom S)) by RELAT_1:36
    .= R * (S * (S \ T)) by Th11
    .= R * {} by Def2
    .= {};
  hence thesis by A1;
end;

theorem
  ((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
  set R = the entrance of N;
  set S = the escape of N;
  set T = id(the carrier of N);
  (R \ T) * (S \ T) c= R * (S \ T) by RELAT_1:30,XBOOLE_1:36; then
A1: (R \ T) * (S \ T) c= {} by Th15;
  (S \ T) * (S \ T) c= S * (S \ T) by RELAT_1:30,XBOOLE_1:36; then
A2: (S \ T) * (S \ T) c= {} by Def2;
  (S \ T) * (R \ T) c= S * (R \ T) by RELAT_1:30,XBOOLE_1:36; then
A3: (S \ T) * (R \ T) c= {} by Th15;
  (R \ T) * (R \ T) c= R * (R \ T) by RELAT_1:30,XBOOLE_1:36;
  then ((R \ T) * (R \ T)) c= {} by Def2;
  hence thesis by A1,A2,A3,XBOOLE_1:3;
end;

definition
  let N;
  func e_Places(N) -> set equals
  rng (the entrance of N);
  correctness;
end;

definition
  let N;
  func e_Transitions(N) -> set equals
  (the carrier of N) \ e_Places(N);
  correctness;
end;

theorem Th17:
  ([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)
proof
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;
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 thesis by A6,Th13;
  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;
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 thesis by A11,Th13;
  end;
  hence thesis by A1;
end;

theorem Th18:
  (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
A1: for x,y holds [x,y] in (the entrance of N) \ id(the carrier of N)
  implies [x,y] in [:e_Transitions(N),e_Places(N):]
  proof
    let x,y;
    assume
A2: [x,y] in (the entrance of N) \ id(the carrier of 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 thesis by A6,ZFMISC_1:87;
  end;
  for x,y holds [x,y] in (the escape of N) \ id(the carrier of N) implies
  [x,y] in [:e_Transitions(N),e_Places(N):]
  proof
    let x,y;
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);
    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 thesis by ZFMISC_1:87;
  end;
  hence thesis by A1,RELAT_1:def 3;
end;

definition
  let N;
  func e_Flow N -> Relation equals
  ((the entrance of N)~ \/ (the escape of N)) \ id N;
  correctness;
end;

theorem
  e_Flow N c= [:e_Places(N), e_Transitions(N):] \/
    [:e_Transitions(N), e_Places(N):]
proof
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 thesis by A2,XBOOLE_1:13;
end;

definition
  let N;

  func e_pre(N) -> Relation equals
  (the entrance of N) \ id(the carrier of N);
  correctness;
  func e_post(N) -> Relation equals
  (the escape of N) \ id(the carrier of N);
  correctness;
end;

theorem
  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;
  func e_shore(N) -> set equals
  the carrier of N;
  correctness;
  func e_prox(N) -> Relation equals
  ((the entrance of N) \/ (the escape of N))~;
  correctness;
  func e_flow(N) -> Relation equals
  ((the entrance of N)~ \/ (the escape of N)) \/ id(the carrier of N);
  correctness;
end;

theorem
  e_prox(N) c= [:e_shore(N),e_shore(N):] &
  e_flow(N) c= [:e_shore(N),e_shore(N):]
proof
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 thesis by A4,A1,SYSREL:4,XBOOLE_1:8;
end;

theorem
  (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
  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)) = ((R~ \/ S~) \/ (S \/ R))
  \/ T by RELAT_1:23
    .= (((R~ \/ S~) \/ S) \/ R) \/ T by XBOOLE_1:4
    .= ((R~ \/ (S~ \/ S)) \/ R) \/ T by XBOOLE_1:4
    .= (R~ \/ ((S \/ S~) \/ R)) \/ T by XBOOLE_1:4
    .= (R~ \/ (S \/ (S~ \/ R))) \/ T by XBOOLE_1:4
    .= ((R~ \/ S) \/ (S~ \/ R)) \/ T by XBOOLE_1:4
    .= e_flow(N) \/ ((S~ \/ (R~)~) \/ T) by XBOOLE_1:5
    .= e_flow(N) \/ ((R~ \/ S)~ \/ T) by RELAT_1:23
    .= e_flow(N) \/ ((R~ \/ S)~ \/ T~)
    .= e_flow(N) \/ (e_flow(N))~ by RELAT_1:23;
A2: (e_prox(N) \ T) * e_prox(N) = ((R~ \/ S~) \ T) * ((R \/ S)~) by RELAT_1:23
    .= ((R~ \ T) \/ (S~ \ T)) * ((R \/ S)~) by XBOOLE_1:42
    .= ((R~ \ T) \/ (S~ \ T)) * (R~ \/ S~) by RELAT_1:23
    .= (((R~ \ T) \/ (S~ \ T)) * R~) \/ (((R~ \ T) \/ (S~ \ T)) * S~) by
RELAT_1:32
    .= (((R~ \ T) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) \/ (S~ \ T)) * S~)
  by SYSREL:6
    .= (((R~ \ T) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \ T)
  * S~)) by SYSREL:6
    .= (((R~ \ T~) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \ T
  ) * S~))
    .= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \
  T) * S~))
    .= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
  T) * S~))
    .= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
  T~) * S~))
    .= (((R \ T)~ * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
  T~) * S~)) by RELAT_1:24
    .= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \ T
  ~) * S~)) by RELAT_1:24
    .= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S~ \ T~
  ) * S~)) by RELAT_1:24
    .= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S \ T)~
  * S~)) by RELAT_1:24
    .= ((R * (R \ T))~ \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S \ T)~
  * S~)) by RELAT_1:35
    .= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ (((R \ T)~ * S~) \/ ((S \ T)~ *
  S~)) by RELAT_1:35
    .= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ ((S *(R \ T))~ \/ ((S \ T)~ * S
  ~)) by RELAT_1:35
    .= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ (S * (S \ T)
  )~) by RELAT_1:35
    .= (({}~) \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ (S * (S \ T))~) by Def2
    .= (({}~) \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ ({})~) by Def2
    .= ({}~ \/ {}~) \/ ((S * (R \ T))~ \/ {}~) by Th15
    .= {} by Th15;
  (e_prox(N)) * (e_prox(N)) = ((R \/ S) * (R \/ S))~ by RELAT_1:35
    .= (((R \/ S) * R) \/ ((R \/ S) * S))~ by RELAT_1:32
    .= (((R * R) \/ (S * R)) \/ ((R \/ S) * S))~ by SYSREL:6
    .= (((R * R) \/ (S * R)) \/ ((R * S) \/ (S * S)))~ by SYSREL:6
    .= ((R \/ (S * R)) \/ ((R * S) \/ (S * S) ) )~ by Def1
    .= ((R \/ S) \/ ((R * S) \/ (S * S)))~ by Def1
    .= ((R \/ S) \/ (R \/ (S * S)))~ by Def1
    .= ((R \/ S) \/ (R \/ S))~ by Def1
    .= e_prox(N);
  hence thesis by A2,A1;
end;

theorem Th23:
  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
  set T = the entrance of N, C = the carrier of N;
  set E = the escape of N, I = id C;
  for x,y holds [x,y] in (E \ I) implies [x,y] in (id(C \ rng E) * (E \ I))
  proof
    let x,y;
    assume
A1: [x,y] in (E \ I);
    then [x,y] in E by XBOOLE_0:def 5; then
A2: x in dom(E) by XTUPLE_0:def 12;
A3: not x in rng E
    proof
      assume x in rng E;
      then ex z st [z,x] in E by XTUPLE_0:def 13; then
      E * (E \ I) <> {} by A1,RELAT_1:def 8;
      hence thesis by Def2;
    end;
    dom E c= C by Th14;
    then x in (C \ rng E) by A2,A3,XBOOLE_0:def 5;
    then [x,x] in id(C \ rng E) by RELAT_1:def 10;
    hence thesis by A1,RELAT_1:def 8;
  end; then
A4: E \ I c= id(C \ rng E) * (E \ I) by RELAT_1:def 3;
  for x,y holds [x,y] in (T \ I) implies [x,y] in (id(C \ rng T) * (T \ I))
  proof
    let x,y;
    assume
A5: [x,y] in (T \ I);
    then [x,y] in T by XBOOLE_0:def 5; then
A6: x in dom(T) by XTUPLE_0:def 12;
A7: not x in rng T
    proof
      assume x in rng T;
      then ex z st [z,x] in T by XTUPLE_0:def 13;
      then T * (T \ I) <> {} by A5,RELAT_1:def 8;
      hence thesis by Def2;
    end;
    dom T c= C by Th14;
    then x in (C \ rng T) by A6,A7,XBOOLE_0:def 5;
    then [x,x] in id(C \ rng T) by RELAT_1:def 10;
    hence thesis by A5,RELAT_1:def 8;
  end; then
A8: (T \ I) c= id(C \ rng T) * (T \ I) by RELAT_1:def 3;
  id(C \ rng E) * (E \ I) c= (E \ I) &
  id(C \ rng T) * (T \ I) c= (T \ I) by RELAT_1:50;
  hence thesis by A4,A8,XBOOLE_0:def 10;
end;

theorem Th24:
  ((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
  set T = the entrance of N, C = the carrier of N;
  set E = the escape of N, I = id C;
  (T \ I) * (T \ I) c= T * (T \ I) by RELAT_1:30,XBOOLE_1:36; then
A1: (T \ I) * (T \ I) c= {} by Def2;
  (E \ I) * (T \ I) c= E * (T \ I) by RELAT_1:30,XBOOLE_1:36;
  then
A2: (E \ I) * (T \ I) c= {} by Th15;
  (T \ I) * (E \ I) c= T * (E \ I) by RELAT_1:30,XBOOLE_1:36; then
A3: (T \ I) * (E \ I) c= {} by Th15;
  (E \ I) * (E \ I) c= E * (E \ I) by RELAT_1:30,XBOOLE_1:36; then
  (E \ I) * (E \ I) c= {} by Def2;
  hence thesis by A1,A2,A3,XBOOLE_1:3;
end;

theorem Th25:
  ((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
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 thesis by A1;
end;

theorem
  ((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
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 thesis by A1;
end;

theorem Th27:
  ((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
A1: for x,y 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;
    assume [x,y] in ((the entrance of N) \ id(the carrier of N)) * (id((the
    carrier of N) \ rng(the entrance of N)));
    then consider z 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 thesis by A4,XTUPLE_0:def 13;
  end;
  for x,y 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;
    assume [x,y] in ((the escape of N) \ id(the carrier of N)) * (id((the
    carrier of N) \ rng(the escape of N)));
    then consider z 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 thesis by A7,XTUPLE_0:def 13;
  end;
  hence thesis by A1,RELAT_1:37;
end;

theorem Th28:
  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
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 thesis by A1;
end;

definition
  let N;

  func e_entrance(N) -> Relation equals
  (((the escape of N) \ id(the carrier of N))~) \/
    id((the carrier of N) \ rng(the escape of N));
  correctness;
  func e_escape(N) -> Relation equals
  (((the entrance of N) \ id(the carrier of N))~) \/
    id((the carrier of N) \ rng(the entrance of N));
  correctness;
end;

theorem
  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
  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) = ((P~) * ((P~) \/ T)) \/ (T * ((P~) \/ T)
  ) by SYSREL:6
    .= (((P~) * (P~)) \/ ((P~) * T)) \/ (T * ((P~) \/ T)) by RELAT_1:32
    .= (((P~) * (P~)) \/ ((P~) * T)) \/ ((T * (P~)) \/ (T * T)) by RELAT_1:32
    .= (((P * P)~) \/ ((P~) * T)) \/ ((T * (P~)) \/ (T * T)) by RELAT_1:35
    .= (((P * P)~) \/ ((P~) * (T~))) \/ ((T * (P~)) \/ (T * T))
    .= (((P * P)~) \/ ((P~) * (T~))) \/ (((T~) * (P~)) \/ (T * T))
    .= (((P * P)~) \/ ((P~) * (T~))) \/ (((T~) * (P~)) \/ T) by SYSREL:12
    .= (((P * P)~) \/ ((T * P)~)) \/ (((T~) * (P~)) \/ T) by RELAT_1:35
    .= (((P * P)~) \/ ((T * P)~)) \/ (((P * T)~) \/ T) by RELAT_1:35
    .= (({}~) \/ ((T * P)~)) \/ (((P * T)~) \/ T) by Th24
    .= (({}~) \/ (P~)) \/ (((P * T)~) \/ T) by Th23
    .= ({} \/ (P~)) \/ ({} \/ T) by Th27
    .= e_entrance(N);
A2: e_escape(N) * e_escape(N) = ((Q~) * ((Q~) \/ S)) \/ (S * ((Q~) \/ S)) by
SYSREL:6
    .= (((Q~) * (Q~)) \/ ((Q~) * S)) \/ (S * ((Q~) \/ S)) by RELAT_1:32
    .= (((Q~) * (Q~)) \/ ((Q~) * S)) \/ ((S * (Q~)) \/ (S * S)) by RELAT_1:32
    .= (((Q * Q)~) \/ ((Q~) * S)) \/ ((S * (Q~)) \/ (S * S)) by RELAT_1:35
    .= (((Q * Q)~) \/ ((Q~) * (S~))) \/ ((S * (Q~)) \/ (S * S))
    .= (((Q * Q)~) \/ ((Q~) * (S~))) \/ (((S~) * (Q~)) \/ (S * S))
    .= (((Q * Q)~) \/ ((Q~) * (S~))) \/ (((S~) * (Q~)) \/ S) by SYSREL:12
    .= (((Q * Q)~) \/ ((S * Q)~)) \/ (((S~) * (Q~)) \/ S) by RELAT_1:35
    .= (((Q * Q)~) \/ ((S * Q)~)) \/ (((Q * S)~) \/ S) by RELAT_1:35
    .= (({}~) \/ ((S * Q)~)) \/ (((Q * S)~) \/ S) by Th24
    .= (({}~) \/ (Q~)) \/ (((Q * S)~) \/ S) by Th23
    .= ({} \/ (Q~)) \/ ({} \/ S) by Th27
    .= e_escape(N);
A3: e_escape(N) * e_entrance(N) = ((Q~) * ((P~) \/ T)) \/ (S * ((P~) \/ T))
  by SYSREL:6
    .= (((Q~) * (P~)) \/ ((Q~) * T)) \/ (S * ((P~) \/ T)) by RELAT_1:32
    .= (((Q~) * (P~)) \/ ((Q~) * T)) \/ ((S * (P~)) \/ (S * T)) by RELAT_1:32
    .= (((P * Q)~) \/ ((Q~) * T)) \/ ((S * (P~)) \/ (S * T)) by RELAT_1:35
    .= (((P * Q)~) \/ ((Q~) * (T~))) \/ ((S * (P~)) \/ (S * T))
    .= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ (S * T))
    .= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ (S * S)) by Th13
    .= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ S) by SYSREL:12
    .= (((P * Q)~) \/ ((T * Q)~)) \/ (((S~) * (P~)) \/ S) by RELAT_1:35
    .= (((P * Q)~) \/ ((T * Q)~)) \/ (((P * S)~) \/ S) by RELAT_1:35
    .= (((P * Q)~) \/ ((S * Q)~)) \/ (((P * S)~) \/ S) by Th13
    .= (((P * Q)~) \/ ((S * Q)~)) \/ (((P * T)~) \/ S) by Th13
    .= (({}~) \/ ((S * Q)~)) \/ (((P * T)~) \/ S) by Th24
    .= (({}~) \/ (Q~)) \/ (((P * T)~) \/ S) by Th23
    .= ({} \/ (Q~)) \/ ({} \/ S) by Th27
    .= e_escape(N);
  e_entrance(N) * e_escape(N) = ((P~) * ((Q~) \/ S)) \/ (T * ((Q~) \/ S))
  by SYSREL:6
    .= (((P~) * (Q~)) \/ ((P~) * S)) \/ (T * ((Q~) \/ S)) by RELAT_1:32
    .= (((P~) * (Q~)) \/ ((P~) * S)) \/ ((T * (Q~)) \/ (T * S)) by RELAT_1:32
    .= (((Q * P)~) \/ ((P~) * S)) \/ ((T * (Q~)) \/ (T * S)) by RELAT_1:35
    .= (((Q * P)~) \/ ((P~) * (S~))) \/ ((T * (Q~)) \/ (T * S))
    .= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ (T * S))
    .= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ (T * T)) by Th13
    .= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ T) by SYSREL:12
    .= (((Q * P)~) \/ ((S * P)~)) \/ (((T~) * (Q~)) \/ T) by RELAT_1:35
    .= (((Q * P)~) \/ ((S * P)~)) \/ (((Q * T)~) \/ T) by RELAT_1:35
    .= (((Q * P)~) \/ ((T * P)~)) \/ (((Q * T)~) \/ T) by Th13
    .= (((Q * P)~) \/ ((T * P)~)) \/ (((Q * S)~) \/ T) by Th13
    .= (({}~) \/ ((T * P)~)) \/ (((Q * S)~) \/ T) by Th24
    .= (({}~) \/ (P~)) \/ (((Q * S)~) \/ T) by Th23
    .= ({} \/ (P~)) \/ ({} \/ T) by Th27
    .= e_entrance(N);
  hence thesis by A1,A3,A2;
end;

theorem
  e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = {} &
  e_escape(N) * (e_escape(N) \ id(e_shore N)) = {}
proof
  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: S c= R by SYSREL:15,XBOOLE_1:36;
  (Q~) * ((Q~) \ R) c= (Q~) * (Q~) by RELAT_1:29,XBOOLE_1:36;
  then (Q~) * ((Q~) \ R) c= {} by Th25;
  then
A2: (Q~) * ((Q~) \ R) = {} by XBOOLE_1:3;
  S * ((Q~) \ R) c= S * (Q~) by RELAT_1:29,XBOOLE_1:36;
  then S * ((Q~) \ R) c= {} by Th28;
  then
A3: S * ((Q~) \ R) = {} by XBOOLE_1:3;
A4: e_escape(N) * (e_escape(N) \ id(e_shore(N))) = ((Q~) \/ S) * (((Q~) \
  R) \/ (S \ R)) by XBOOLE_1:42
    .= ((Q~) \/ S) * (((Q~) \ R) \/ {}) by A1,XBOOLE_1:37
    .= {} \/ {} by A2,A3,SYSREL:6
    .= {};
A5: T c= R by SYSREL:15,XBOOLE_1:36;
  T * ((P~) \ R) c= T * (P~) by RELAT_1:29,XBOOLE_1:36;
  then T * ((P~) \ R) c= {} by Th28;
  then
A6: T * ((P~) \ R) = {} by XBOOLE_1:3;
  (P~) * ((P~) \ R) c= (P~) * (P~) by RELAT_1:29,XBOOLE_1:36;
  then (P~) * ((P~) \ R) c= {} by Th25;
  then
A7: (P~) * ((P~) \ R) = {} by XBOOLE_1:3;
  e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = ((P~) \/ T) * (((P
  ~) \ R) \/ (T \ R)) by XBOOLE_1:42
    .= ((P~) \/ T) * (((P~) \ R) \/ {}) by A5,XBOOLE_1:37
    .= {} \/ {} by A7,A6,SYSREL:6
    .= {};
  hence thesis by A4;
end;

definition
  let N;

  func e_adjac(N) -> Relation equals
  (((the entrance of N) \/ (the escape of N)) \ id(the carrier of N))
   \/ id((the carrier of N) \ rng(the entrance of N));
  correctness;
end;

theorem
  e_adjac(N) c= [:e_shore(N),e_shore(N):] &
  e_flow(N) c= [:e_shore(N),e_shore(N):]
proof
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 thesis by A5,A4,XBOOLE_1:8;
end;

theorem
  (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
  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: S c= R by SYSREL:15,XBOOLE_1:36;
  (e_adjac N \/ (e_adjac N)~) = (((P \/ Q) \ R) \/ S) \/ ( (((P \/ Q) \ R
  )~) \/ (S~)) by RELAT_1:23
    .= (((P \/ Q) \ R) \/ S) \/ ( ( ((P \/ Q) \ R)~) \/ S)
    .= (((P \/ Q) \ R) \/ ( ((P \/ Q) \ R)~ ) ) \/ S by XBOOLE_1:5
    .= (((P \/ Q) \ R) \/ ( ((P \/ Q)~) \ (R~) )) \/ S by RELAT_1:24
    .= (((P \/ Q) \ R) \/ (((P \/ Q)~) \ R)) \/ S
    .= (((P \/ Q) \/ ((P \/ Q)~)) \ R) \/ S by XBOOLE_1:42;
  then
A2: (e_adjac(N) \/ (e_adjac(N))~) \/ id(e_shore(N)) = (((P \/ Q) \/ ((P
  \/ Q)~)) \ R) \/ (S \/ R) by XBOOLE_1:4
    .= (((P \/ Q) \/ ((P \/ Q)~)) \ R) \/ R by A1,XBOOLE_1:12
    .= (((P~ \/ (Q~)) \/ (P \/ Q)) \ R) \/ R by RELAT_1:23
    .= (P~ \/ ((Q \/ P) \/ (Q~)) \ R) \/ R by XBOOLE_1:4
    .= (P~ \/ (Q \/ (P \/ (Q~))) \ R) \/ R by XBOOLE_1:4
    .= ( ( (P~ \/ Q) \/ (P \/ (Q~)) ) \ R) \/ R by XBOOLE_1:4
    .= ( (P~ \/ Q) \/ (P \/ (Q~)) ) \/ R by XBOOLE_1:39
    .= e_flow N \/ ((((P \/ (Q~))~)~) \/ R) by XBOOLE_1:5
    .= e_flow N \/ (((P~ \/ ((Q~)~))~) \/ R) by RELAT_1:23
    .= e_flow N \/ (((P~ \/ Q)~) \/ (R~))
    .= e_flow N \/ (e_flow N)~ by RELAT_1:23;
  S c= R by SYSREL:15,XBOOLE_1:36;
  then
A3: S \ R = {} by XBOOLE_1:37;
  (P \ R) * (Q \ R) c= P * (Q \ R) by RELAT_1:30,XBOOLE_1:36;
  then (P \ R) * (Q \ R) c= {} by Th15;
  then
A4: (P \ R) * (Q \ R) = {} by XBOOLE_1:3;
  (P \ R) * (P \ R) c= P * (P \ R) by RELAT_1:30,XBOOLE_1:36;
  then (P \ R) * (P \ R) c= {} by Def2;
  then
A5: (P \ R) * (P \ R) = {} by XBOOLE_1:3;
  (Q \ R) * (P \ R) c= Q * (P \ R) by RELAT_1:30,XBOOLE_1:36;
  then (Q \ R) * (P \ R) c= {} by Th15;
  then
A6: (Q \ R) * (P \ R) = {} by XBOOLE_1:3;
  (Q \ R) * (Q \ R) c= Q * (Q \ R) by RELAT_1:30,XBOOLE_1:36;
  then (Q \ R) * (Q \ R) c= {} by Def2;
  then
A7: (Q \ R) * (Q \ R) = {} by XBOOLE_1:3;
A8: (e_adjac(N) \ R) * e_adjac(N) = (((((P \/ Q) \ R) \/ S
  ) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S) by RELAT_1:32
    .= (((((P \ R) \/ (Q \ R)) \/ S) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q)
  \ R) \/ S) \ R) * S) by XBOOLE_1:42
    .= ((( (((P \ R) \/ (Q \ R)) \ R) \/ (S \ R)) * ((P \/ Q) \ R)) \/ ((((P
  \/ Q) \ R) \/ S) \ R) * S) by XBOOLE_1:42
    .= (((( ( ((P \ R) \ R) \/ ((Q \ R) \ R)) ) \/ (S \ R)) * ((P \/ Q) \ R)
  ) \/ ((((P \/ Q) \ R) \/ S) \ R) * S) by XBOOLE_1:42
    .= (((((((P \ (R \/ R)) \/ ((Q \ R) \ R))) \/ (S \ R)) * ((P \/ Q) \ R))
  \/ ((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1:41
    .= ((((((P \ R) \/ ((Q \ (R \/ R))) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((
  (P \/ Q) \ R) \/ S) \ R) * S))) by XBOOLE_1:41
    .= (((((P \ R) \/ (Q \ R)) \/ (S \ R)) * ((P \ R) \/ (Q \ R)) \/ ((((P
  \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1:42
    .= (((((P \ R) \/ (Q \ R) \/ (S \ R)) * ((P \ R) \/ (Q \ R))) \/ ((((P \
  R) \/ (Q \ R)) \/ S) \ R) * S)) by XBOOLE_1:42
    .= ((( ( ( ((P \ R) \/ (Q \ R)) \/ (S \ R) ) * (P \ R) ) \/ ( ( ((P \ R)
\/ (Q \ R)) \/ (S \ R) ) * (Q \ R))) \/ ((((P \ R) \/ (Q \ R)) \/ S) \ R) * S))
  by RELAT_1:32
    .= ((( ( ( ((P \ R) \/ (Q \ R)) \/ (S \ R) ) * (P \ R) ) \/ ( ( ((P \ R)
\/ (Q \ R)) * (Q \ R) ) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/ (Q \ R)) \/
  S) \ R) * S)) by SYSREL:6
    .= ((( ( ( ((P \ R) \/ (Q \ R)) * (P \ R)) \/ ((S \ R) ) * (P \ R)) ) \/
( ( ((P \ R) \/ (Q \ R)) * (Q \ R)) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/
  (Q \ R)) \/ S) \ R) * S) by SYSREL:6
    .= ((( ( ({} \/ {}) \/ ((S \ R) ) * (P \ R)) ) \/ ( ( ((P \ R) \/ (Q \ R
)) * (Q \ R)) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/ (Q \ R)) \/ S) \ R) *
  S) by A5,A6,SYSREL:6
    .= ((( {} * (P \ R)) \/ ({} * (Q \ R))) \/ ((((P \ R) \/ (Q \ R)) \/ S)
  \ R) * S) by A3,A4,A7,SYSREL:6
    .= ( ( ((P \ R) \/ (Q \ R)) \ R) \/ (S \ R) ) * S by XBOOLE_1:42
    .= ( ( ((P \ R) \ R) \/ ((Q \ R) \ R)) \/ (S \ R) ) * S by XBOOLE_1:42
    .= ( ((P \ (R \/ R)) \/ ((Q \ R) \ R)) \/ (S \ R) ) * S by XBOOLE_1:41
    .= ( ((P \ R) \/ (Q \ (R \/ R)) ) \/ (S \ R) ) * S by XBOOLE_1:41
    .= ((P \ R) * S) \/ ((Q \ R) * S) by A3,SYSREL:6
    .= {} \/ ((Q \ R) * S) by Th27
    .= {} \/ ((Q \ R) * T) by Th13
    .= {} by Th27;
  e_adjac(N) * e_adjac(N) = ((((P \/ Q) \ R) * (((P \/ Q) \ R) \/ S)) \/
  (S * (((P \/ Q) \ R) \/ S))) by SYSREL:6
    .= ((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ (S * (
  ((P \/ Q) \ R) \/ S)) by RELAT_1:32
    .= ((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ ((S *
  ((P \/ Q) \ R)) \/ (S * S)) by RELAT_1:32
    .= ((((P \ R) \/ (Q \ R)) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/
  ((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
    .= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \/ Q) \ R) * S
  )) \/ ((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
    .= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R
  )) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
    .= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R
  )) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S)) by XBOOLE_1:42
    .= ((((P \ R) \/ (Q \ R)) * ((P \ R)) \/ (((P \ R) \/ (Q \ R)) * (Q \ R)
)) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))
by RELAT_1:32
    .= ((({} \/ {}) \/ (((P \ R) \/ (Q \ R)) * (Q \ R))) \/ (((P \ R) \/ (Q
  \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S)) by A5,A6,SYSREL:6
    .= {} \/ (((P \ R) \/ (Q \ R)) * S) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S
  * S)) by A4,A7,SYSREL:6
    .= (((P \ R) \/ (Q \ R)) * S) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S) by
SYSREL:12
    .= (((P \ R) * S) \/ ((Q \ R) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S)
  by SYSREL:6
    .= (((P \ R) * S) \/ ((Q \ R) * S)) \/ ((S * (P \ R)) \/ (S * (Q \ R))
  \/ S) by RELAT_1:32
    .= ({} \/ ((Q \ R) * S)) \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th27
    .= ((Q \ R) * T) \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th13
    .= {} \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th27
    .= ((P \ R) \/ (S * (Q \ R)) \/ S) by Th23
    .= ((P \ R) \/ (T * (Q \ R)) \/ S) by Th13
    .= ((P \ R) \/ (Q \ R)) \/ S by Th23
    .= e_adjac N by XBOOLE_1:42;
  hence thesis by A8,A2;
end;

reserve N for e_net;

theorem Th33:
  ((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
  (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 thesis by SYSREL:4;
end;

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

theorem
  s_post(N) c= [:e_Places(N),e_Transitions(N):] &
  s_pre(N) c= [:e_Places(N),e_Transitions(N):] by Th33;