:: FF_SIEC semantic presentation

begin


definition
let X, Y be set ;
assume A1: X misses Y ;
func PTempty_f_net (X,Y) ->  strict Pnet equals :Def1: :: FF_SIEC:def 1
 PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);
correctness
coherence
PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #) is strict Pnet;
proof
set M = PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);
 Flow PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #) c= [: the carrier of PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #), the carrier' of PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #):] \/ [: the carrier' of PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #), the carrier of PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #):] by XBOOLE_1:13;
hence  PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #) is strict Pnet by A1, NET_1:def_2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines PTempty_f_net FF_SIEC:def_1_:_
 for X, Y being set st X misses Y holds
PTempty_f_net (X,Y) = PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);

definition
let X be set ;
func Tempty_f_net X ->  strict Pnet equals :: FF_SIEC:def 2
 PTempty_f_net (X,{});
correctness
coherence
PTempty_f_net (X,{}) is strict Pnet;
;
func Pempty_f_net X ->  strict Pnet equals :: FF_SIEC:def 3
 PTempty_f_net ({},X);
correctness
coherence
PTempty_f_net ({},X) is strict Pnet;
;
end;

:: deftheorem  defines Tempty_f_net FF_SIEC:def_2_:_
 for X being set holds Tempty_f_net X = PTempty_f_net (X,{});

:: deftheorem  defines Pempty_f_net FF_SIEC:def_3_:_
 for X being set holds Pempty_f_net X = PTempty_f_net ({},X);

definition
let x be set ;
func Tsingle_f_net x ->  strict Pnet equals :: FF_SIEC:def 4
 PTempty_f_net ({},{x});
correctness
coherence
PTempty_f_net ({},{x}) is strict Pnet;
;
func Psingle_f_net x ->  strict Pnet equals :: FF_SIEC:def 5
 PTempty_f_net ({x},{});
correctness
coherence
PTempty_f_net ({x},{}) is strict Pnet;
;
end;

:: deftheorem  defines Tsingle_f_net FF_SIEC:def_4_:_
 for x being set holds Tsingle_f_net x = PTempty_f_net ({},{x});

:: deftheorem  defines Psingle_f_net FF_SIEC:def_5_:_
 for x being set holds Psingle_f_net x = PTempty_f_net ({x},{});

definition
func empty_f_net  ->  strict Pnet equals :: FF_SIEC:def 6
 PTempty_f_net ({},{});
correctness
coherence
PTempty_f_net ({},{}) is strict Pnet;
;
end;

:: deftheorem  defines empty_f_net FF_SIEC:def_6_:_
 empty_f_net = PTempty_f_net ({},{});

theorem :: FF_SIEC:1
for X, Y being set st X misses Y holds
( the carrier of (PTempty_f_net (X,Y)) = X & the carrier' of (PTempty_f_net (X,Y)) = Y & Flow (PTempty_f_net (X,Y)) = {} )
proof
let X, Y be set ; ::_thesis: ( X misses Y implies ( the carrier of (PTempty_f_net (X,Y)) = X & the carrier' of (PTempty_f_net (X,Y)) = Y & Flow (PTempty_f_net (X,Y)) = {} ) )
assume  X misses Y ; ::_thesis: ( the carrier of (PTempty_f_net (X,Y)) = X & the carrier' of (PTempty_f_net (X,Y)) = Y & Flow (PTempty_f_net (X,Y)) = {} )
then  PTempty_f_net (X,Y) = PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #) by Def1;
hence  ( the carrier of (PTempty_f_net (X,Y)) = X & the carrier' of (PTempty_f_net (X,Y)) = Y & Flow (PTempty_f_net (X,Y)) = {} ) ; ::_thesis: verum
end;

theorem :: FF_SIEC:2
for X being set holds
( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} )
proof
let X be set ; ::_thesis: ( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} )
 Tempty_f_net X = PT_net_Str(# X,{},({} (X,{})),({} ({},X)) #) by Def1, XBOOLE_1:65;
hence  ( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} ) ; ::_thesis: verum
end;

theorem :: FF_SIEC:3
for X being set holds
( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} )
proof
let X be set ; ::_thesis: ( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} )
 {} misses X by XBOOLE_1:65;
then  Pempty_f_net X = PT_net_Str(# {},X,({} ({},X)),({} (X,{})) #) by Def1;
hence  ( the carrier of (Pempty_f_net X) = {} & the carrier' of (Pempty_f_net X) = X & Flow (Pempty_f_net X) = {} ) ; ::_thesis: verum
end;

theorem :: FF_SIEC:4
for x being set holds
( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} )
proof
let x be set ; ::_thesis: ( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} )
 {} misses {x} by XBOOLE_1:65;
then  Tsingle_f_net x = PT_net_Str(# {},{x},({} ({},{x})),({} ({x},{})) #) by Def1;
hence  ( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} ) ; ::_thesis: verum
end;

theorem :: FF_SIEC:5
for x being set holds
( the carrier of (Psingle_f_net x) = {x} & the carrier' of (Psingle_f_net x) = {} & Flow (Psingle_f_net x) = {} )
proof
let x be set ; ::_thesis: ( the carrier of (Psingle_f_net x) = {x} & the carrier' of (Psingle_f_net x) = {} & Flow (Psingle_f_net x) = {} )
 Psingle_f_net x = PT_net_Str(# {x},{},({} ({x},{})),({} ({},{x})) #) by Def1, XBOOLE_1:65;
hence  ( the carrier of (Psingle_f_net x) = {x} & the carrier' of (Psingle_f_net x) = {} & Flow (Psingle_f_net x) = {} ) ; ::_thesis: verum
end;

theorem :: FF_SIEC:6
( the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & Flow empty_f_net = {} )
proof
 empty_f_net = PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) by Def1, XBOOLE_1:65;
hence  ( the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & Flow empty_f_net = {} ) ; ::_thesis: verum
end;

theorem Th7: :: FF_SIEC:7
for x, y being set
for M being Pnet holds
( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
proof
let x, y be set ; ::_thesis: for M being Pnet holds
( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
let M be Pnet; ::_thesis: ( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) )
A1: the carrier of M misses the carrier' of M by NET_1:def_2;
 Flow M c= [: the carrier of M, the carrier' of M:] \/ [: the carrier' of M, the carrier of M:] by NET_1:def_2;
hence  ( ( [x,y] in Flow M & x in the carrier' of M implies ( not x in the carrier of M & not y in the carrier' of M & y in the carrier of M ) ) & ( [x,y] in Flow M & y in the carrier' of M implies ( not y in the carrier of M & not x in the carrier' of M & x in the carrier of M ) ) & ( [x,y] in Flow M & x in the carrier of M implies ( not y in the carrier of M & not x in the carrier' of M & y in the carrier' of M ) ) & ( [x,y] in Flow M & y in the carrier of M implies ( not x in the carrier of M & not y in the carrier' of M & x in the carrier' of M ) ) ) by A1, SYSREL:7; ::_thesis: verum
end;

theorem Th8: :: FF_SIEC:8
for M being Pnet holds
( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] )
proof
let M be Pnet; ::_thesis: ( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] )
A1: the carrier of M c= Elements M by XBOOLE_1:7;
A2: the carrier' of M c= Elements M by XBOOLE_1:7;
then A3: [: the carrier of M, the carrier' of M:] c= [:(Elements M),(Elements M):] by A1, ZFMISC_1:96;
 [: the carrier' of M, the carrier of M:] c= [:(Elements M),(Elements M):] by A1, A2, ZFMISC_1:96;
then A4: [: the carrier of M, the carrier' of M:] \/ [: the carrier' of M, the carrier of M:] c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:8;
 Flow M c= [: the carrier of M, the carrier' of M:] \/ [: the carrier' of M, the carrier of M:] by NET_1:def_2;
then  Flow M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
hence  ( Flow M c= [:(Elements M),(Elements M):] & (Flow M) ~ c= [:(Elements M),(Elements M):] ) by SYSREL:4; ::_thesis: verum
end;

theorem Th9: :: FF_SIEC:9
for M being Pnet holds
( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M )
proof
let M be Pnet; ::_thesis: ( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M )
A1: for x being set st x in rng ((Flow M) | the carrier' of M) holds
x in the carrier of M
proof
let x be set ; ::_thesis: ( x in rng ((Flow M) | the carrier' of M) implies x in the carrier of M )
assume  x in rng ((Flow M) | the carrier' of M) ; ::_thesis: x in the carrier of M
then consider y being set  such that
A2: [y,x] in (Flow M) | the carrier' of M by XTUPLE_0:def_13;
A3: y in the carrier' of M by A2, RELAT_1:def_11;
 [y,x] in Flow M by A2, RELAT_1:def_11;
hence  x in the carrier of M by A3, Th7; ::_thesis: verum
end;
A4: for x being set st x in rng (((Flow M) ~) | the carrier' of M) holds
x in the carrier of M
proof
let x be set ; ::_thesis: ( x in rng (((Flow M) ~) | the carrier' of M) implies x in the carrier of M )
assume  x in rng (((Flow M) ~) | the carrier' of M) ; ::_thesis: x in the carrier of M
then consider y being set  such that
A5: [y,x] in ((Flow M) ~) | the carrier' of M by XTUPLE_0:def_13;
A6: [y,x] in (Flow M) ~ by A5, RELAT_1:def_11;
A7: y in the carrier' of M by A5, RELAT_1:def_11;
 [x,y] in Flow M by A6, RELAT_1:def_7;
hence  x in the carrier of M by A7, Th7; ::_thesis: verum
end;
A8: for x being set st x in rng ((Flow M) | the carrier of M) holds
x in the carrier' of M
proof
let x be set ; ::_thesis: ( x in rng ((Flow M) | the carrier of M) implies x in the carrier' of M )
assume  x in rng ((Flow M) | the carrier of M) ; ::_thesis: x in the carrier' of M
then consider y being set  such that
A9: [y,x] in (Flow M) | the carrier of M by XTUPLE_0:def_13;
A10: y in the carrier of M by A9, RELAT_1:def_11;
 [y,x] in Flow M by A9, RELAT_1:def_11;
hence  x in the carrier' of M by A10, Th7; ::_thesis: verum
end;
 for x being set st x in rng (((Flow M) ~) | the carrier of M) holds
x in the carrier' of M
proof
let x be set ; ::_thesis: ( x in rng (((Flow M) ~) | the carrier of M) implies x in the carrier' of M )
assume  x in rng (((Flow M) ~) | the carrier of M) ; ::_thesis: x in the carrier' of M
then consider y being set  such that
A11: [y,x] in ((Flow M) ~) | the carrier of M by XTUPLE_0:def_13;
A12: [y,x] in (Flow M) ~ by A11, RELAT_1:def_11;
A13: y in the carrier of M by A11, RELAT_1:def_11;
 [x,y] in Flow M by A12, RELAT_1:def_7;
hence  x in the carrier' of M by A13, Th7; ::_thesis: verum
end;
hence  ( rng ((Flow M) | the carrier' of M) c= the carrier of M & rng (((Flow M) ~) | the carrier' of M) c= the carrier of M & rng ((Flow M) | the carrier of M) c= the carrier' of M & rng (((Flow M) ~) | the carrier of M) c= the carrier' of M & rng (id the carrier' of M) c= the carrier' of M & dom (id the carrier' of M) c= the carrier' of M & rng (id the carrier of M) c= the carrier of M & dom (id the carrier of M) c= the carrier of M ) by A1, A4, A8, TARSKI:def_3; ::_thesis: verum
end;

Lm1:  for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C
proof
let A, B, C, D be set ; ::_thesis: ( B misses D & A c= B & C c= D implies A misses C )
assume that
A1: B misses D and
A2: A c= B and
A3: C c= D ; ::_thesis: A misses C
assume  A meets C ; ::_thesis: contradiction
then A4: ex x being set st x in A /\ C by XBOOLE_0:4;
 A /\ C c= B /\ D by A2, A3, XBOOLE_1:27;
hence  contradiction by A1, A4, XBOOLE_0:4; ::_thesis: verum
end;

theorem Th10: :: FF_SIEC:10
for M being Pnet holds
( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) )
proof
let M be Pnet; ::_thesis: ( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) )
set R = (Flow M) | the carrier' of M;
set S = ((Flow M) ~) | the carrier' of M;
set T = id the carrier' of M;
set R1 = (Flow M) | the carrier of M;
set S1 = ((Flow M) ~) | the carrier of M;
set T1 = id the carrier of M;
A1: dom ((Flow M) | the carrier' of M) c= the carrier' of M by RELAT_1:58;
A2: rng ((Flow M) | the carrier' of M) c= the carrier of M by Th9;
A3: dom (((Flow M) ~) | the carrier' of M) c= the carrier' of M by RELAT_1:58;
A4: rng (((Flow M) ~) | the carrier' of M) c= the carrier of M by Th9;
A5: dom ((Flow M) | the carrier of M) c= the carrier of M by RELAT_1:58;
A6: rng ((Flow M) | the carrier of M) c= the carrier' of M by Th9;
A7: dom (((Flow M) ~) | the carrier of M) c= the carrier of M by RELAT_1:58;
A8: rng (((Flow M) ~) | the carrier of M) c= the carrier' of M by Th9;
 the carrier of M misses the carrier' of M by NET_1:def_2;
hence  ( rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) & rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom ((Flow M) | the carrier' of M) misses rng (id the carrier of M) & dom (((Flow M) ~) | the carrier' of M) misses rng ((Flow M) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (((Flow M) ~) | the carrier' of M) & dom (((Flow M) ~) | the carrier' of M) misses rng (id the carrier of M) & rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) & rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) & dom ((Flow M) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) & dom (((Flow M) ~) | the carrier of M) misses rng ((Flow M) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (((Flow M) ~) | the carrier of M) & dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) ) by A1, A2, A3, A4, A5, A6, A7, A8, Lm1; ::_thesis: verum
end;

theorem Th11: :: FF_SIEC:11
for M being Pnet holds
( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} )
proof
let M be Pnet; ::_thesis: ( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} )
A1: rng ((Flow M) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) by Th10;
A2: rng (((Flow M) ~) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) by Th10;
A3: rng ((Flow M) | the carrier' of M) misses dom (((Flow M) ~) | the carrier' of M) by Th10;
A4: rng (((Flow M) ~) | the carrier' of M) misses dom ((Flow M) | the carrier' of M) by Th10;
A5: rng ((Flow M) | the carrier of M) misses dom ((Flow M) | the carrier of M) by Th10;
A6: rng (((Flow M) ~) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) by Th10;
A7: rng ((Flow M) | the carrier of M) misses dom (((Flow M) ~) | the carrier of M) by Th10;
 rng (((Flow M) ~) | the carrier of M) misses dom ((Flow M) | the carrier of M) by Th10;
hence  ( ((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M) = {} & ((Flow M) | the carrier of M) * ((Flow M) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M) = {} ) by A1, A2, A3, A4, A5, A6, A7, RELAT_1:44; ::_thesis: verum
end;

theorem Th12: :: FF_SIEC:12
for M being Pnet holds
( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} )
proof
let M be Pnet; ::_thesis: ( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} )
A1: rng ((Flow M) | the carrier' of M) c= the carrier of M by Th9;
A2: rng (((Flow M) ~) | the carrier' of M) c= the carrier of M by Th9;
A3: rng ((Flow M) | the carrier of M) c= the carrier' of M by Th9;
A4: rng (((Flow M) ~) | the carrier of M) c= the carrier' of M by Th9;
A5: dom ((Flow M) | the carrier of M) misses rng (id the carrier' of M) by Th10;
A6: dom (((Flow M) ~) | the carrier of M) misses rng (id the carrier' of M) by Th10;
A7: rng ((Flow M) | the carrier of M) misses dom (id the carrier of M) by Th10;
A8: rng (((Flow M) ~) | the carrier of M) misses dom (id the carrier of M) by Th10;
A9: rng (id the carrier of M) misses dom ((Flow M) | the carrier' of M) by Th10;
A10: rng (id the carrier of M) misses dom (((Flow M) ~) | the carrier' of M) by Th10;
A11: rng ((Flow M) | the carrier' of M) misses dom (id the carrier' of M) by Th10;
 rng (((Flow M) ~) | the carrier' of M) misses dom (id the carrier' of M) by Th10;
hence  ( ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M & (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M & (id the carrier' of M) * ((Flow M) | the carrier' of M) = (Flow M) | the carrier' of M & (id the carrier' of M) * (((Flow M) ~) | the carrier' of M) = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier of M) * ((Flow M) | the carrier of M) = (Flow M) | the carrier of M & (id the carrier of M) * (((Flow M) ~) | the carrier of M) = ((Flow M) ~) | the carrier of M & ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M & (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M & (id the carrier' of M) * ((Flow M) | the carrier of M) = {} & (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} & ((Flow M) | the carrier of M) * (id the carrier of M) = {} & (((Flow M) ~) | the carrier of M) * (id the carrier of M) = {} & (id the carrier of M) * ((Flow M) | the carrier' of M) = {} & (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} & ((Flow M) | the carrier' of M) * (id the carrier' of M) = {} & (((Flow M) ~) | the carrier' of M) * (id the carrier' of M) = {} ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, RELAT_1:44, RELAT_1:51, RELAT_1:53, RELAT_1:58; ::_thesis: verum
end;

theorem Th13: :: FF_SIEC:13
for M being Pnet holds
( ((Flow M) ~) | the carrier' of M misses id (Elements M) & (Flow M) | the carrier' of M misses id (Elements M) & ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )
proof
let M be Pnet; ::_thesis: ( ((Flow M) ~) | the carrier' of M misses id (Elements M) & (Flow M) | the carrier' of M misses id (Elements M) & ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )
set T = id (Elements M);
thus  ((Flow M) ~) | the carrier' of M misses id (Elements M) ::_thesis: ( (Flow M) | the carrier' of M misses id (Elements M) & ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )
proof
set R = ((Flow M) ~) | the carrier' of M;
 for x, y being set holds not [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id (Elements M))
proof
let x, y be set ; ::_thesis: not [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id (Elements M))
assume A1: [x,y] in (((Flow M) ~) | the carrier' of M) /\ (id (Elements M)) ; ::_thesis: contradiction
then A2: [x,y] in ((Flow M) ~) | the carrier' of M by XBOOLE_0:def_4;
A3: [x,y] in id (Elements M) by A1, XBOOLE_0:def_4;
A4: [x,y] in (Flow M) ~ by A2, RELAT_1:def_11;
A5: x in the carrier' of M by A2, RELAT_1:def_11;
 [y,x] in Flow M by A4, RELAT_1:def_7;
then  x <> y by A5, Th7;
hence  contradiction by A3, RELAT_1:def_10; ::_thesis: verum
end;
then  (((Flow M) ~) | the carrier' of M) /\ (id (Elements M)) = {} by RELAT_1:37;
hence  ((Flow M) ~) | the carrier' of M misses id (Elements M) by XBOOLE_0:def_7; ::_thesis: verum
end;
thus  (Flow M) | the carrier' of M misses id (Elements M) ::_thesis: ( ((Flow M) ~) | the carrier of M misses id (Elements M) & (Flow M) | the carrier of M misses id (Elements M) )
proof
set R = (Flow M) | the carrier' of M;
 for x, y being set holds not [x,y] in ((Flow M) | the carrier' of M) /\ (id (Elements M))
proof
let x, y be set ; ::_thesis: not [x,y] in ((Flow M) | the carrier' of M) /\ (id (Elements M))
assume A6: [x,y] in ((Flow M) | the carrier' of M) /\ (id (Elements M)) ; ::_thesis: contradiction
then A7: [x,y] in (Flow M) | the carrier' of M by XBOOLE_0:def_4;
A8: [x,y] in id (Elements M) by A6, XBOOLE_0:def_4;
A9: x in the carrier' of M by A7, RELAT_1:def_11;
 [x,y] in Flow M by A7, RELAT_1:def_11;
then  x <> y by A9, Th7;
hence  contradiction by A8, RELAT_1:def_10; ::_thesis: verum
end;
then  ((Flow M) | the carrier' of M) /\ (id (Elements M)) = {} by RELAT_1:37;
hence  (Flow M) | the carrier' of M misses id (Elements M) by XBOOLE_0:def_7; ::_thesis: verum
end;
thus  ((Flow M) ~) | the carrier of M misses id (Elements M) ::_thesis: (Flow M) | the carrier of M misses id (Elements M)
proof
set R = ((Flow M) ~) | the carrier of M;
 for x, y being set holds not [x,y] in (((Flow M) ~) | the carrier of M) /\ (id (Elements M))
proof
let x, y be set ; ::_thesis: not [x,y] in (((Flow M) ~) | the carrier of M) /\ (id (Elements M))
assume A10: [x,y] in (((Flow M) ~) | the carrier of M) /\ (id (Elements M)) ; ::_thesis: contradiction
then A11: [x,y] in ((Flow M) ~) | the carrier of M by XBOOLE_0:def_4;
A12: [x,y] in id (Elements M) by A10, XBOOLE_0:def_4;
A13: [x,y] in (Flow M) ~ by A11, RELAT_1:def_11;
A14: x in the carrier of M by A11, RELAT_1:def_11;
 [y,x] in Flow M by A13, RELAT_1:def_7;
then  x <> y by A14, Th7;
hence  contradiction by A12, RELAT_1:def_10; ::_thesis: verum
end;
then  (((Flow M) ~) | the carrier of M) /\ (id (Elements M)) = {} by RELAT_1:37;
hence  ((Flow M) ~) | the carrier of M misses id (Elements M) by XBOOLE_0:def_7; ::_thesis: verum
end;
set R = (Flow M) | the carrier of M;
 for x, y being set holds not [x,y] in ((Flow M) | the carrier of M) /\ (id (Elements M))
proof
let x, y be set ; ::_thesis: not [x,y] in ((Flow M) | the carrier of M) /\ (id (Elements M))
assume A15: [x,y] in ((Flow M) | the carrier of M) /\ (id (Elements M)) ; ::_thesis: contradiction
then A16: [x,y] in (Flow M) | the carrier of M by XBOOLE_0:def_4;
A17: [x,y] in id (Elements M) by A15, XBOOLE_0:def_4;
A18: x in the carrier of M by A16, RELAT_1:def_11;
 [x,y] in Flow M by A16, RELAT_1:def_11;
then  x <> y by A18, Th7;
hence  contradiction by A17, RELAT_1:def_10; ::_thesis: verum
end;
then  ((Flow M) | the carrier of M) /\ (id (Elements M)) = {} by RELAT_1:37;
hence  (Flow M) | the carrier of M misses id (Elements M) by XBOOLE_0:def_7; ::_thesis: verum
end;

theorem Th14: :: FF_SIEC:14
for M being Pnet holds
( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M )
proof
let M be Pnet; ::_thesis: ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M )
A1: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M
proof
set R = ((Flow M) ~) | the carrier' of M;
set S = id the carrier of M;
set T = id (Elements M);
A2: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A3: ((Flow M) ~) | the carrier' of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ {} by A2, XBOOLE_1:37
.= ((Flow M) ~) | the carrier' of M by A3, XBOOLE_1:83 ;
hence  ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M ; ::_thesis: verum
end;
A4: (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = id (Elements M);
A5: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A6: (Flow M) | the carrier' of M misses id (Elements M) by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ {} by A5, XBOOLE_1:37
.= (Flow M) | the carrier' of M by A6, XBOOLE_1:83 ;
hence  (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ; ::_thesis: verum
end;
A7: ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M
proof
set R = ((Flow M) ~) | the carrier of M;
set S = id the carrier of M;
set T = id (Elements M);
A8: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A9: ((Flow M) ~) | the carrier of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ {} by A8, XBOOLE_1:37
.= ((Flow M) ~) | the carrier of M by A9, XBOOLE_1:83 ;
hence  ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M ; ::_thesis: verum
end;
A10: (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M
proof
set R = (Flow M) | the carrier of M;
set S = id the carrier of M;
set T = id (Elements M);
A11: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A12: (Flow M) | the carrier of M misses id (Elements M) by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (((Flow M) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id (Elements M))) \/ {} by A11, XBOOLE_1:37
.= (Flow M) | the carrier of M by A12, XBOOLE_1:83 ;
hence  (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M ; ::_thesis: verum
end;
A13: ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M
proof
set R = ((Flow M) ~) | the carrier of M;
set S = id the carrier' of M;
set T = id (Elements M);
A14: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A15: ((Flow M) ~) | the carrier of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier of M) \ (id (Elements M))) \/ {} by A14, XBOOLE_1:37
.= ((Flow M) ~) | the carrier of M by A15, XBOOLE_1:83 ;
hence  ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M ; ::_thesis: verum
end;
A16: (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M
proof
set R = (Flow M) | the carrier of M;
set S = id the carrier' of M;
set T = id (Elements M);
A17: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A18: (Flow M) | the carrier of M misses id (Elements M) by Th13;
(((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (((Flow M) | the carrier of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier of M) \ (id (Elements M))) \/ {} by A17, XBOOLE_1:37
.= (Flow M) | the carrier of M by A18, XBOOLE_1:83 ;
hence  (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M ; ::_thesis: verum
end;
A19: ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M
proof
set R = ((Flow M) ~) | the carrier' of M;
set S = id the carrier' of M;
set T = id (Elements M);
A20: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A21: ((Flow M) ~) | the carrier' of M misses id (Elements M) by Th13;
((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= ((((Flow M) ~) | the carrier' of M) \ (id (Elements M))) \/ {} by A20, XBOOLE_1:37
.= ((Flow M) ~) | the carrier' of M by A21, XBOOLE_1:83 ;
hence  ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M ; ::_thesis: verum
end;
 (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier' of M;
set T = id (Elements M);
A22: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A23: (Flow M) | the carrier' of M misses id (Elements M) by Th13;
(((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ ((id the carrier' of M) \ (id (Elements M))) by XBOOLE_1:42
.= (((Flow M) | the carrier' of M) \ (id (Elements M))) \/ {} by A22, XBOOLE_1:37
.= (Flow M) | the carrier' of M by A23, XBOOLE_1:83 ;
hence  (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ; ::_thesis: verum
end;
hence  ( ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier of M & (((Flow M) | the carrier of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier of M & ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = ((Flow M) ~) | the carrier' of M & (((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M)) = (Flow M) | the carrier' of M ) by A1, A4, A7, A10, A13, A16, A19; ::_thesis: verum
end;

theorem Th15: :: FF_SIEC:15
for M being Pnet holds
( ((Flow M) | the carrier of M) ~ = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier' of M) ~ = ((Flow M) ~) | the carrier of M )
proof
let M be Pnet; ::_thesis: ( ((Flow M) | the carrier of M) ~ = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier' of M) ~ = ((Flow M) ~) | the carrier of M )
set R = Flow M;
set X = the carrier of M;
set Y = the carrier' of M;
 for x, y being set st [x,y] in ((Flow M) | the carrier of M) ~ holds
[x,y] in ((Flow M) ~) | the carrier' of M
proof
let x, y be set ; ::_thesis: ( [x,y] in ((Flow M) | the carrier of M) ~ implies [x,y] in ((Flow M) ~) | the carrier' of M )
assume  [x,y] in ((Flow M) | the carrier of M) ~ ; ::_thesis: [x,y] in ((Flow M) ~) | the carrier' of M
then A1: [y,x] in (Flow M) | the carrier of M by RELAT_1:def_7;
then A2: [y,x] in Flow M by RELAT_1:def_11;
A3: y in the carrier of M by A1, RELAT_1:def_11;
A4: [x,y] in (Flow M) ~ by A2, RELAT_1:def_7;
 x in the carrier' of M by A2, A3, Th7;
hence  [x,y] in ((Flow M) ~) | the carrier' of M by A4, RELAT_1:def_11; ::_thesis: verum
end;
then A5: ((Flow M) | the carrier of M) ~ c= ((Flow M) ~) | the carrier' of M by RELAT_1:def_3;
 for x, y being set st [x,y] in ((Flow M) ~) | the carrier' of M holds
[x,y] in ((Flow M) | the carrier of M) ~
proof
let x, y be set ; ::_thesis: ( [x,y] in ((Flow M) ~) | the carrier' of M implies [x,y] in ((Flow M) | the carrier of M) ~ )
assume A6: [x,y] in ((Flow M) ~) | the carrier' of M ; ::_thesis: [x,y] in ((Flow M) | the carrier of M) ~
then  [x,y] in (Flow M) ~ by RELAT_1:def_11;
then A7: [y,x] in Flow M by RELAT_1:def_7;
 x in the carrier' of M by A6, RELAT_1:def_11;
then  y in the carrier of M by A7, Th7;
then  [y,x] in (Flow M) | the carrier of M by A7, RELAT_1:def_11;
hence  [x,y] in ((Flow M) | the carrier of M) ~ by RELAT_1:def_7; ::_thesis: verum
end;
then A8: ((Flow M) ~) | the carrier' of M c= ((Flow M) | the carrier of M) ~ by RELAT_1:def_3;
 for x, y being set st [x,y] in ((Flow M) | the carrier' of M) ~ holds
[x,y] in ((Flow M) ~) | the carrier of M
proof
let x, y be set ; ::_thesis: ( [x,y] in ((Flow M) | the carrier' of M) ~ implies [x,y] in ((Flow M) ~) | the carrier of M )
assume  [x,y] in ((Flow M) | the carrier' of M) ~ ; ::_thesis: [x,y] in ((Flow M) ~) | the carrier of M
then A9: [y,x] in (Flow M) | the carrier' of M by RELAT_1:def_7;
then A10: [y,x] in Flow M by RELAT_1:def_11;
A11: y in the carrier' of M by A9, RELAT_1:def_11;
A12: [x,y] in (Flow M) ~ by A10, RELAT_1:def_7;
 x in the carrier of M by A10, A11, Th7;
hence  [x,y] in ((Flow M) ~) | the carrier of M by A12, RELAT_1:def_11; ::_thesis: verum
end;
then A13: ((Flow M) | the carrier' of M) ~ c= ((Flow M) ~) | the carrier of M by RELAT_1:def_3;
 for x, y being set st [x,y] in ((Flow M) ~) | the carrier of M holds
[x,y] in ((Flow M) | the carrier' of M) ~
proof
let x, y be set ; ::_thesis: ( [x,y] in ((Flow M) ~) | the carrier of M implies [x,y] in ((Flow M) | the carrier' of M) ~ )
assume A14: [x,y] in ((Flow M) ~) | the carrier of M ; ::_thesis: [x,y] in ((Flow M) | the carrier' of M) ~
then  [x,y] in (Flow M) ~ by RELAT_1:def_11;
then A15: [y,x] in Flow M by RELAT_1:def_7;
 x in the carrier of M by A14, RELAT_1:def_11;
then  y in the carrier' of M by A15, Th7;
then  [y,x] in (Flow M) | the carrier' of M by A15, RELAT_1:def_11;
hence  [x,y] in ((Flow M) | the carrier' of M) ~ by RELAT_1:def_7; ::_thesis: verum
end;
then  ((Flow M) ~) | the carrier of M c= ((Flow M) | the carrier' of M) ~ by RELAT_1:def_3;
hence  ( ((Flow M) | the carrier of M) ~ = ((Flow M) ~) | the carrier' of M & ((Flow M) | the carrier' of M) ~ = ((Flow M) ~) | the carrier of M ) by A5, A8, A13, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th16: :: FF_SIEC:16
for M being Pnet holds
( ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M & ((Flow M) | the carrier' of M) \/ ((Flow M) | the carrier of M) = Flow M & (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) = (Flow M) ~ & (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) = (Flow M) ~ )
proof
let M be Pnet; ::_thesis: ( ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M & ((Flow M) | the carrier' of M) \/ ((Flow M) | the carrier of M) = Flow M & (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) = (Flow M) ~ & (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) = (Flow M) ~ )
set R = Flow M;
 Flow M c= [:(Elements M),(Elements M):] by Th8;
then  ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M by SYSREL:9;
hence  ( ((Flow M) | the carrier of M) \/ ((Flow M) | the carrier' of M) = Flow M & ((Flow M) | the carrier' of M) \/ ((Flow M) | the carrier of M) = Flow M & (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) = (Flow M) ~ & (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) = (Flow M) ~ ) by RELAT_1:23; ::_thesis: verum
end;

definition
let M be Pnet;
func f_enter M ->  Relation equals :: FF_SIEC:def 7
(((Flow M) ~) | the carrier' of M) \/ (id the carrier of M);
correctness
coherence
(((Flow M) ~) | the carrier' of M) \/ (id the carrier of M) is Relation;
;
func f_exit M ->  Relation equals :: FF_SIEC:def 8
((Flow M) | the carrier' of M) \/ (id the carrier of M);
correctness
coherence
((Flow M) | the carrier' of M) \/ (id the carrier of M) is Relation;
;
end;

:: deftheorem  defines f_enter FF_SIEC:def_7_:_
 for M being Pnet holds f_enter M = (((Flow M) ~) | the carrier' of M) \/ (id the carrier of M);

:: deftheorem  defines f_exit FF_SIEC:def_8_:_
 for M being Pnet holds f_exit M = ((Flow M) | the carrier' of M) \/ (id the carrier of M);

theorem :: FF_SIEC:17
for M being Pnet holds
( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
proof
let M be Pnet; ::_thesis: ( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
A1: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
 id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A2: id the carrier of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: (Flow M) | the carrier' of M c= Flow M by RELAT_1:59;
 Flow M c= [:(Elements M),(Elements M):] by Th8;
then  (Flow M) | the carrier' of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
hence  f_exit M c= [:(Elements M),(Elements M):] by A2, XBOOLE_1:8; ::_thesis: f_enter M c= [:(Elements M),(Elements M):]
A4: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
 id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A5: id the carrier of M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
A6: ((Flow M) ~) | the carrier' of M c= (Flow M) ~ by RELAT_1:59;
 (Flow M) ~ c= [:(Elements M),(Elements M):] by Th8;
then  ((Flow M) ~) | the carrier' of M c= [:(Elements M),(Elements M):] by A6, XBOOLE_1:1;
hence  f_enter M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:8; ::_thesis: verum
end;

theorem :: FF_SIEC:18
for M being Pnet holds
( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )
proof
let M be Pnet; ::_thesis: ( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )
A1: for x being set st x in dom (f_exit M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in dom (f_exit M) implies x in Elements M )
assume  x in dom (f_exit M) ; ::_thesis: x in Elements M
then  x in (dom ((Flow M) | the carrier' of M)) \/ (dom (id the carrier of M)) by RELAT_1:1;
then  ( x in dom ((Flow M) | the carrier' of M) or x in dom (id the carrier of M) ) by XBOOLE_0:def_3;
then  ( x in the carrier' of M or x in the carrier of M ) by RELAT_1:57;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
A2: for x being set st x in rng (f_exit M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in rng (f_exit M) implies x in Elements M )
assume  x in rng (f_exit M) ; ::_thesis: x in Elements M
then A3: x in (rng ((Flow M) | the carrier' of M)) \/ (rng (id the carrier of M)) by RELAT_1:12;
A4: ( x in rng ((Flow M) | the carrier' of M) implies x in Elements M )
proof
assume  x in rng ((Flow M) | the carrier' of M) ; ::_thesis: x in Elements M
then consider y being set  such that
A5: [y,x] in (Flow M) | the carrier' of M by XTUPLE_0:def_13;
A6: y in the carrier' of M by A5, RELAT_1:def_11;
 [y,x] in Flow M by A5, RELAT_1:def_11;
then  ( x in the carrier' of M or x in the carrier of M ) by A6, Th7;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( x in rng (id the carrier of M) implies x in Elements M )
proof
assume  x in rng (id the carrier of M) ; ::_thesis: x in Elements M
then  ( x in the carrier' of M or x in the carrier of M ) ;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in Elements M by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
A7: for x being set st x in dom (f_enter M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in dom (f_enter M) implies x in Elements M )
assume  x in dom (f_enter M) ; ::_thesis: x in Elements M
then  x in (dom (((Flow M) ~) | the carrier' of M)) \/ (dom (id the carrier of M)) by RELAT_1:1;
then  ( x in dom (((Flow M) ~) | the carrier' of M) or x in dom (id the carrier of M) ) by XBOOLE_0:def_3;
then  ( x in the carrier' of M or x in the carrier of M ) by RELAT_1:57;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 for x being set st x in rng (f_enter M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in rng (f_enter M) implies x in Elements M )
assume  x in rng (f_enter M) ; ::_thesis: x in Elements M
then A8: x in (rng (((Flow M) ~) | the carrier' of M)) \/ (rng (id the carrier of M)) by RELAT_1:12;
A9: ( x in rng (((Flow M) ~) | the carrier' of M) implies x in Elements M )
proof
assume  x in rng (((Flow M) ~) | the carrier' of M) ; ::_thesis: x in Elements M
then consider y being set  such that
A10: [y,x] in ((Flow M) ~) | the carrier' of M by XTUPLE_0:def_13;
A11: [y,x] in (Flow M) ~ by A10, RELAT_1:def_11;
A12: y in the carrier' of M by A10, RELAT_1:def_11;
 [x,y] in Flow M by A11, RELAT_1:def_7;
then  ( x in the carrier' of M or x in the carrier of M ) by A12, Th7;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( x in rng (id the carrier of M) implies x in Elements M )
proof
assume  x in rng (id the carrier of M) ; ::_thesis: x in Elements M
then  ( x in the carrier' of M or x in the carrier of M ) ;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in Elements M by A8, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  ( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M ) by A1, A2, A7, TARSKI:def_3; ::_thesis: verum
end;

theorem :: FF_SIEC:19
for M being Pnet holds
( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )
proof
let M be Pnet; ::_thesis: ( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )
A1: (f_exit M) * (f_exit M) = f_exit M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
A2: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th12;
A3: ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M by Th12;
A4: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:12;
(f_exit M) * (f_exit M) = (((Flow M) | the carrier' of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) \/ ((id the carrier of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) by SYSREL:6
.= ((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ (((Flow M) | the carrier' of M) * (id the carrier of M))) \/ ((id the carrier of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) by RELAT_1:32
.= ((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ (((Flow M) | the carrier' of M) * (id the carrier of M))) \/ (((id the carrier of M) * ((Flow M) | the carrier' of M)) \/ ((id the carrier of M) * (id the carrier of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A2, A3, A4, Th11
.= f_exit M ;
hence  (f_exit M) * (f_exit M) = f_exit M ; ::_thesis: verum
end;
A5: (f_exit M) * (f_enter M) = f_exit M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = ((Flow M) ~) | the carrier' of M;
A6: (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} by Th12;
A7: ((Flow M) | the carrier' of M) * (id the carrier of M) = (Flow M) | the carrier' of M by Th12;
A8: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:12;
(f_exit M) * (f_enter M) = (((Flow M) | the carrier' of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) \/ ((id the carrier of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) by SYSREL:6
.= ((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ (((Flow M) | the carrier' of M) * (id the carrier of M))) \/ ((id the carrier of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) by RELAT_1:32
.= ((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ (((Flow M) | the carrier' of M) * (id the carrier of M))) \/ (((id the carrier of M) * (((Flow M) ~) | the carrier' of M)) \/ ((id the carrier of M) * (id the carrier of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A6, A7, A8, Th11
.= f_exit M ;
hence  (f_exit M) * (f_enter M) = f_exit M ; ::_thesis: verum
end;
A9: (f_enter M) * (f_enter M) = f_enter M
proof
set R = ((Flow M) ~) | the carrier' of M;
set S = id the carrier of M;
A10: (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} by Th12;
A11: (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M by Th12;
A12: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:12;
(f_enter M) * (f_enter M) = ((((Flow M) ~) | the carrier' of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) \/ ((id the carrier of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier of M))) \/ ((id the carrier of M) * ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier of M))) \/ (((id the carrier of M) * (((Flow M) ~) | the carrier' of M)) \/ ((id the carrier of M) * (id the carrier of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A10, A11, A12, Th11
.= f_enter M ;
hence  (f_enter M) * (f_enter M) = f_enter M ; ::_thesis: verum
end;
 (f_enter M) * (f_exit M) = f_enter M
proof
set R = (Flow M) | the carrier' of M;
set S = id the carrier of M;
set T = ((Flow M) ~) | the carrier' of M;
A13: (((Flow M) ~) | the carrier' of M) * (id the carrier of M) = ((Flow M) ~) | the carrier' of M by Th12;
A14: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th12;
A15: (id the carrier of M) * (id the carrier of M) = id the carrier of M by SYSREL:12;
(f_enter M) * (f_exit M) = ((((Flow M) ~) | the carrier' of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) \/ ((id the carrier of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier of M))) \/ ((id the carrier of M) * (((Flow M) | the carrier' of M) \/ (id the carrier of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier of M))) \/ (((id the carrier of M) * ((Flow M) | the carrier' of M)) \/ ((id the carrier of M) * (id the carrier of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier' of M)) \/ ({} \/ (id the carrier of M)) by A13, A14, A15, Th11
.= f_enter M ;
hence  (f_enter M) * (f_exit M) = f_enter M ; ::_thesis: verum
end;
hence  ( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M ) by A1, A5, A9; ::_thesis: verum
end;

theorem :: FF_SIEC:20
for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )
proof
let M be Pnet; ::_thesis: ( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )
set S = id the carrier of M;
thus  (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} ::_thesis: (f_enter M) * ((f_enter M) \ (id (Elements M))) = {}
proof
set R = (Flow M) | the carrier' of M;
A1: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th12;
(f_exit M) * ((f_exit M) \ (id (Elements M))) = (((Flow M) | the carrier' of M) \/ (id the carrier of M)) * ((Flow M) | the carrier' of M) by Th14
.= (((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((id the carrier of M) * ((Flow M) | the carrier' of M)) by SYSREL:6
.= {} by A1, Th11 ;
hence  (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} ; ::_thesis: verum
end;
set R = ((Flow M) ~) | the carrier' of M;
A2: (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} by Th12;
(f_enter M) * ((f_enter M) \ (id (Elements M))) = ((((Flow M) ~) | the carrier' of M) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier' of M) by Th14
.= ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier' of M)) by SYSREL:6
.= {} by A2, Th11 ;
hence  (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} ; ::_thesis: verum
end;

definition
let M be Pnet;
func f_prox M ->  Relation equals :: FF_SIEC:def 9
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M);
correctness
coherence
(((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M) is Relation;
;
func f_flow M ->  Relation equals :: FF_SIEC:def 10
(Flow M) \/ (id (Elements M));
correctness
coherence
(Flow M) \/ (id (Elements M)) is Relation;
;
end;

:: deftheorem  defines f_prox FF_SIEC:def_9_:_
 for M being Pnet holds f_prox M = (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M);

:: deftheorem  defines f_flow FF_SIEC:def_10_:_
 for M being Pnet holds f_flow M = (Flow M) \/ (id (Elements M));

theorem :: FF_SIEC:21
for M being Pnet holds
( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~)) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~) )
proof
let M be Pnet; ::_thesis: ( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~)) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~) )
set R = (Flow M) | the carrier of M;
set S = ((Flow M) ~) | the carrier of M;
set T = id the carrier of M;
set Q = id (Elements M);
A1: ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \ (id (Elements M)) = ((((Flow M) | the carrier of M) \/ (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) \/ (id the carrier of M))) \ (id (Elements M)) by XBOOLE_1:5
.= ((((Flow M) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M))) \/ (((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M))) by XBOOLE_1:42
.= ((Flow M) | the carrier of M) \/ (((((Flow M) ~) | the carrier of M) \/ (id the carrier of M)) \ (id (Elements M))) by Th14
.= ((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M) by Th14 ;
A2: (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) = ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * ((Flow M) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M)) by RELAT_1:32
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M)) by SYSREL:6
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) by SYSREL:6
.= ({} \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) by Th11
.= ({} \/ {}) \/ ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) by Th11
.= ({} \/ {}) \/ ({} \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) by Th11
.= {} by Th11 ;
A3: ((Flow M) | the carrier of M) \/ ((((Flow M) ~) | the carrier of M) ~) = ((Flow M) | the carrier of M) \/ ((((Flow M) | the carrier' of M) ~) ~) by Th15
.= Flow M by Th16 ;
A4: (((Flow M) | the carrier of M) ~) \/ (((Flow M) ~) | the carrier of M) = (((Flow M) | the carrier of M) ~) \/ (((Flow M) | the carrier' of M) ~) by Th15
.= (Flow M) ~ by Th16 ;
A5: ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~) \/ (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) = ((((Flow M) | the carrier of M) ~) \/ ((((Flow M) ~) | the carrier of M) ~)) \/ (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) by RELAT_1:23
.= ((((Flow M) | the carrier of M) ~) \/ ((((Flow M) ~) | the carrier of M) \/ ((Flow M) | the carrier of M))) \/ ((((Flow M) ~) | the carrier of M) ~) by XBOOLE_1:4
.= (((((Flow M) | the carrier of M) ~) \/ (((Flow M) ~) | the carrier of M)) \/ ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) ~) by XBOOLE_1:4
.= (Flow M) \/ ((Flow M) ~) by A3, A4, XBOOLE_1:4 ;
A6: (f_prox M) \/ ((f_prox M) ~) = ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~) \/ ((id the carrier of M) ~)) by RELAT_1:23
.= (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) ~) by XBOOLE_1:4
.= (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ (id the carrier of M)) \/ ((id the carrier of M) ~) by XBOOLE_1:4
.= ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) \/ ((id the carrier of M) ~)) by XBOOLE_1:4
.= ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) ~)) \/ ((id the carrier of M) \/ (id the carrier of M))
.= ((Flow M) \/ ((Flow M) ~)) \/ (id the carrier of M) by A5 ;
A7: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A8: (f_prox M) * (f_prox M) = (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by RELAT_1:32
.= ((((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * ((Flow M) | the carrier of M)) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by RELAT_1:32
.= ((((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * ((Flow M) | the carrier of M)) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by SYSREL:6
.= ((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by SYSREL:6
.= ((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by SYSREL:6
.= ((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (id the carrier of M)) * (id the carrier of M)) by SYSREL:6
.= ((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (id the carrier of M)) \/ ((id the carrier of M) * (id the carrier of M))) by SYSREL:6
.= ((((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by SYSREL:6
.= ((({} \/ ((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M))) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th11
.= ((({} \/ {}) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th11
.= ((({} \/ {}) \/ ((id the carrier of M) * ((Flow M) | the carrier of M))) \/ (({} \/ ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th11
.= (((id the carrier of M) * ((Flow M) | the carrier of M)) \/ ({} \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M)))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th11
.= (((Flow M) | the carrier of M) \/ ((id the carrier of M) * (((Flow M) ~) | the carrier of M))) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th12
.= (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ ((id the carrier of M) * (id the carrier of M))) by Th12
.= (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (((((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ (id the carrier of M)) by SYSREL:12
.= (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ (({} \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M))) \/ (id the carrier of M)) by Th12
.= (((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier of M)) by Th12
.= f_prox M ;
A9: ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} \/ ((((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M)) * (id the carrier of M)) by A1, A2, RELAT_1:32
.= (((Flow M) | the carrier of M) * (id the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M)) by SYSREL:6
.= {} \/ ((((Flow M) ~) | the carrier of M) * (id the carrier of M)) by Th12
.= {} by Th12 ;
((f_prox M) \/ ((f_prox M) ~)) \/ (id (Elements M)) = ((Flow M) \/ ((Flow M) ~)) \/ ((id the carrier of M) \/ (id (Elements M))) by A6, XBOOLE_1:4
.= ((Flow M) \/ ((Flow M) ~)) \/ (id (Elements M)) by A7, XBOOLE_1:12
.= ((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ (id (Elements M))) by XBOOLE_1:5
.= ((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ ((id (Elements M)) ~))
.= (f_flow M) \/ ((f_flow M) ~) by RELAT_1:23 ;
hence  ( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~)) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~) ) by A8, A9; ::_thesis: verum
end;

definition
let M be Pnet;
func f_places M ->  set  equals :: FF_SIEC:def 11
 the carrier of M;
correctness
coherence
the carrier of M is set ;
;
func f_transitions M ->  set  equals :: FF_SIEC:def 12
 the carrier' of M;
correctness
coherence
the carrier' of M is set ;
;
func f_pre M ->  Relation equals :: FF_SIEC:def 13
(Flow M) | the carrier' of M;
correctness
coherence
(Flow M) | the carrier' of M is Relation;
;
func f_post M ->  Relation equals :: FF_SIEC:def 14
((Flow M) ~) | the carrier' of M;
correctness
coherence
((Flow M) ~) | the carrier' of M is Relation;
;
end;

:: deftheorem  defines f_places FF_SIEC:def_11_:_
 for M being Pnet holds f_places M = the carrier of M;

:: deftheorem  defines f_transitions FF_SIEC:def_12_:_
 for M being Pnet holds f_transitions M = the carrier' of M;

:: deftheorem  defines f_pre FF_SIEC:def_13_:_
 for M being Pnet holds f_pre M = (Flow M) | the carrier' of M;

:: deftheorem  defines f_post FF_SIEC:def_14_:_
 for M being Pnet holds f_post M = ((Flow M) ~) | the carrier' of M;

theorem :: FF_SIEC:22
for M being Pnet holds
( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )
proof
let M be Pnet; ::_thesis: ( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )
A1: for x, y being set st [x,y] in f_pre M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x, y be set ; ::_thesis: ( [x,y] in f_pre M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume A2: [x,y] in f_pre M ; ::_thesis: [x,y] in [:(f_transitions M),(f_places M):]
then A3: x in the carrier' of M by RELAT_1:def_11;
 [x,y] in Flow M by A2, RELAT_1:def_11;
then  y in the carrier of M by A3, Th7;
hence  [x,y] in [:(f_transitions M),(f_places M):] by A3, ZFMISC_1:87; ::_thesis: verum
end;
 for x, y being set st [x,y] in f_post M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x, y be set ; ::_thesis: ( [x,y] in f_post M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume A4: [x,y] in f_post M ; ::_thesis: [x,y] in [:(f_transitions M),(f_places M):]
then A5: [x,y] in (Flow M) ~ by RELAT_1:def_11;
A6: x in the carrier' of M by A4, RELAT_1:def_11;
 [y,x] in Flow M by A5, RELAT_1:def_7;
then  y in the carrier of M by A6, Th7;
hence  [x,y] in [:(f_transitions M),(f_places M):] by A6, ZFMISC_1:87; ::_thesis: verum
end;
hence  ( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] ) by A1, RELAT_1:def_3; ::_thesis: verum
end;

theorem :: FF_SIEC:23
for M being Pnet holds
( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
proof
let M be Pnet; ::_thesis: ( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
A1: (Flow M) | the carrier of M c= Flow M by RELAT_1:59;
 Flow M c= [:(Elements M),(Elements M):] by Th8;
then A2: (Flow M) | the carrier of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: ((Flow M) ~) | the carrier of M c= (Flow M) ~ by RELAT_1:59;
 (Flow M) ~ c= [:(Elements M),(Elements M):] by Th8;
then A4: ((Flow M) ~) | the carrier of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
 the carrier of M c= Elements M by XBOOLE_1:7;
then A5: [: the carrier of M, the carrier of M:] c= [:(Elements M),(Elements M):] by ZFMISC_1:96;
 id the carrier of M c= [: the carrier of M, the carrier of M:] by RELSET_1:13;
then A6: id the carrier of M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:1;
 ((Flow M) | the carrier of M) \/ (((Flow M) ~) | the carrier of M) c= [:(Elements M),(Elements M):] by A2, A4, XBOOLE_1:8;
hence  f_prox M c= [:(Elements M),(Elements M):] by A6, XBOOLE_1:8; ::_thesis: f_flow M c= [:(Elements M),(Elements M):]
A7: Flow M c= [:(Elements M),(Elements M):] by Th8;
 id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
hence  f_flow M c= [:(Elements M),(Elements M):] by A7, XBOOLE_1:8; ::_thesis: verum
end;

definition
let M be Pnet;
func f_entrance M ->  Relation equals :: FF_SIEC:def 15
(((Flow M) ~) | the carrier of M) \/ (id the carrier' of M);
correctness
coherence
(((Flow M) ~) | the carrier of M) \/ (id the carrier' of M) is Relation;
;
func f_escape M ->  Relation equals :: FF_SIEC:def 16
((Flow M) | the carrier of M) \/ (id the carrier' of M);
correctness
coherence
((Flow M) | the carrier of M) \/ (id the carrier' of M) is Relation;
;
end;

:: deftheorem  defines f_entrance FF_SIEC:def_15_:_
 for M being Pnet holds f_entrance M = (((Flow M) ~) | the carrier of M) \/ (id the carrier' of M);

:: deftheorem  defines f_escape FF_SIEC:def_16_:_
 for M being Pnet holds f_escape M = ((Flow M) | the carrier of M) \/ (id the carrier' of M);

theorem :: FF_SIEC:24
for M being Pnet holds
( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )
proof
let M be Pnet; ::_thesis: ( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )
A1: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
 id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A2: id the carrier' of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: (Flow M) | the carrier of M c= Flow M by RELAT_1:59;
 Flow M c= [:(Elements M),(Elements M):] by Th8;
then  (Flow M) | the carrier of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
hence  f_escape M c= [:(Elements M),(Elements M):] by A2, XBOOLE_1:8; ::_thesis: f_entrance M c= [:(Elements M),(Elements M):]
A4: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
 id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A5: id the carrier' of M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
A6: ((Flow M) ~) | the carrier of M c= (Flow M) ~ by RELAT_1:59;
 (Flow M) ~ c= [:(Elements M),(Elements M):] by Th8;
then  ((Flow M) ~) | the carrier of M c= [:(Elements M),(Elements M):] by A6, XBOOLE_1:1;
hence  f_entrance M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:8; ::_thesis: verum
end;

theorem :: FF_SIEC:25
for M being Pnet holds
( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )
proof
let M be Pnet; ::_thesis: ( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )
A1: for x being set st x in dom (f_escape M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in dom (f_escape M) implies x in Elements M )
assume  x in dom (f_escape M) ; ::_thesis: x in Elements M
then  x in (dom ((Flow M) | the carrier of M)) \/ (dom (id the carrier' of M)) by RELAT_1:1;
then  ( x in dom ((Flow M) | the carrier of M) or x in dom (id the carrier' of M) ) by XBOOLE_0:def_3;
then  ( x in the carrier of M or x in the carrier' of M ) by RELAT_1:57;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
A2: for x being set st x in rng (f_escape M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in rng (f_escape M) implies x in Elements M )
assume  x in rng (f_escape M) ; ::_thesis: x in Elements M
then A3: x in (rng ((Flow M) | the carrier of M)) \/ (rng (id the carrier' of M)) by RELAT_1:12;
A4: ( x in rng ((Flow M) | the carrier of M) implies x in Elements M )
proof
assume  x in rng ((Flow M) | the carrier of M) ; ::_thesis: x in Elements M
then consider y being set  such that
A5: [y,x] in (Flow M) | the carrier of M by XTUPLE_0:def_13;
A6: y in the carrier of M by A5, RELAT_1:def_11;
 [y,x] in Flow M by A5, RELAT_1:def_11;
then  ( x in the carrier of M or x in the carrier' of M ) by A6, Th7;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( x in rng (id the carrier' of M) implies x in Elements M )
proof
assume  x in rng (id the carrier' of M) ; ::_thesis: x in Elements M
then  ( x in the carrier of M or x in the carrier' of M ) ;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in Elements M by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
A7: for x being set st x in dom (f_entrance M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in dom (f_entrance M) implies x in Elements M )
assume  x in dom (f_entrance M) ; ::_thesis: x in Elements M
then  x in (dom (((Flow M) ~) | the carrier of M)) \/ (dom (id the carrier' of M)) by RELAT_1:1;
then  ( x in dom (((Flow M) ~) | the carrier of M) or x in dom (id the carrier' of M) ) by XBOOLE_0:def_3;
then  ( x in the carrier of M or x in the carrier' of M ) by RELAT_1:57;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 for x being set st x in rng (f_entrance M) holds
x in Elements M
proof
let x be set ; ::_thesis: ( x in rng (f_entrance M) implies x in Elements M )
assume  x in rng (f_entrance M) ; ::_thesis: x in Elements M
then A8: x in (rng (((Flow M) ~) | the carrier of M)) \/ (rng (id the carrier' of M)) by RELAT_1:12;
A9: ( x in rng (((Flow M) ~) | the carrier of M) implies x in Elements M )
proof
assume  x in rng (((Flow M) ~) | the carrier of M) ; ::_thesis: x in Elements M
then consider y being set  such that
A10: [y,x] in ((Flow M) ~) | the carrier of M by XTUPLE_0:def_13;
A11: [y,x] in (Flow M) ~ by A10, RELAT_1:def_11;
A12: y in the carrier of M by A10, RELAT_1:def_11;
 [x,y] in Flow M by A11, RELAT_1:def_7;
then  ( x in the carrier of M or x in the carrier' of M ) by A12, Th7;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
 ( x in rng (id the carrier' of M) implies x in Elements M )
proof
assume  x in rng (id the carrier' of M) ; ::_thesis: x in Elements M
then  ( x in the carrier of M or x in the carrier' of M ) ;
hence  x in Elements M by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  x in Elements M by A8, A9, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  ( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M ) by A1, A2, A7, TARSKI:def_3; ::_thesis: verum
end;

theorem :: FF_SIEC:26
for M being Pnet holds
( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )
proof
let M be Pnet; ::_thesis: ( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )
set R = (Flow M) | the carrier of M;
set S = id the carrier' of M;
A1: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
A2: ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M by Th12;
A3: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
A4: (f_escape M) * (f_escape M) = (((Flow M) | the carrier of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= ((((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A1, A2, A3, Th11
.= f_escape M ;
A5: (f_escape M) * (f_entrance M) = f_escape M
proof
set T = ((Flow M) ~) | the carrier of M;
A6: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
A7: ((Flow M) | the carrier of M) * (id the carrier' of M) = (Flow M) | the carrier of M by Th12;
A8: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_escape M) * (f_entrance M) = (((Flow M) | the carrier of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= ((((Flow M) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ (((Flow M) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ ((Flow M) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A6, A7, A8, Th11
.= f_escape M ;
hence  (f_escape M) * (f_entrance M) = f_escape M ; ::_thesis: verum
end;
A9: (f_entrance M) * (f_entrance M) = f_entrance M
proof
set R = ((Flow M) ~) | the carrier of M;
A10: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
A11: (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M by Th12;
A12: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_entrance M) * (f_entrance M) = ((((Flow M) ~) | the carrier of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A10, A11, A12, Th11
.= f_entrance M ;
hence  (f_entrance M) * (f_entrance M) = f_entrance M ; ::_thesis: verum
end;
 (f_entrance M) * (f_escape M) = f_entrance M
proof
set T = ((Flow M) ~) | the carrier of M;
A13: (((Flow M) ~) | the carrier of M) * (id the carrier' of M) = ((Flow M) ~) | the carrier of M by Th12;
A14: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
A15: (id the carrier' of M) * (id the carrier' of M) = id the carrier' of M by SYSREL:12;
(f_entrance M) * (f_escape M) = ((((Flow M) ~) | the carrier of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by SYSREL:6
.= (((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) | the carrier of M) \/ (id the carrier' of M))) by RELAT_1:32
.= (((((Flow M) ~) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((((Flow M) ~) | the carrier of M) * (id the carrier' of M))) \/ (((id the carrier' of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by RELAT_1:32
.= ({} \/ (((Flow M) ~) | the carrier of M)) \/ ({} \/ (id the carrier' of M)) by A13, A14, A15, Th11
.= f_entrance M ;
hence  (f_entrance M) * (f_escape M) = f_entrance M ; ::_thesis: verum
end;
hence  ( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M ) by A4, A5, A9; ::_thesis: verum
end;

theorem :: FF_SIEC:27
for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )
proof
let M be Pnet; ::_thesis: ( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )
set R = (Flow M) | the carrier of M;
set S = id the carrier' of M;
A1: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
(f_escape M) * ((f_escape M) \ (id (Elements M))) = (((Flow M) | the carrier of M) \/ (id the carrier' of M)) * ((Flow M) | the carrier of M) by Th14
.= (((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * ((Flow M) | the carrier of M)) by SYSREL:6
.= {} by A1, Th11 ;
hence  (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} ; ::_thesis: (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {}
set R = ((Flow M) ~) | the carrier of M;
A2: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
(f_entrance M) * ((f_entrance M) \ (id (Elements M))) = ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) * (((Flow M) ~) | the carrier of M) by Th14
.= ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) by SYSREL:6
.= {} by A2, Th11 ;
hence  (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} ; ::_thesis: verum
end;

notation
let M be Pnet;
synonym  f_circulation M for  f_flow M;
end;

definition
let M be Pnet;
func f_adjac M ->  Relation equals :: FF_SIEC:def 17
(((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M);
correctness
coherence
(((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M) is Relation;
;
end;

:: deftheorem  defines f_adjac FF_SIEC:def_17_:_
 for M being Pnet holds f_adjac M = (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M);

theorem :: FF_SIEC:28
for M being Pnet holds
( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~)) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~) )
proof
let M be Pnet; ::_thesis: ( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~)) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~) )
set R = (Flow M) | the carrier' of M;
set S = ((Flow M) ~) | the carrier' of M;
set T = id the carrier' of M;
set Q = id (Elements M);
A1: ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) \ (id (Elements M)) = ((((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M))) \ (id (Elements M)) by XBOOLE_1:5
.= ((((Flow M) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M))) \/ (((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M))) by XBOOLE_1:42
.= ((Flow M) | the carrier' of M) \/ (((((Flow M) ~) | the carrier' of M) \/ (id the carrier' of M)) \ (id (Elements M))) by Th14
.= ((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M) by Th14 ;
A2: (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) = ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (((Flow M) ~) | the carrier' of M)) by RELAT_1:32
.= ((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (((Flow M) ~) | the carrier' of M)) by SYSREL:6
.= ((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) by SYSREL:6
.= ({} \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) by Th11
.= ({} \/ {}) \/ ((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) by Th11
.= ({} \/ {}) \/ ({} \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) by Th11
.= {} by Th11 ;
A3: ((Flow M) | the carrier' of M) \/ ((((Flow M) ~) | the carrier' of M) ~) = ((Flow M) | the carrier' of M) \/ ((((Flow M) | the carrier of M) ~) ~) by Th15
.= Flow M by Th16 ;
A4: (((Flow M) | the carrier' of M) ~) \/ (((Flow M) ~) | the carrier' of M) = (((Flow M) | the carrier' of M) ~) \/ (((Flow M) | the carrier of M) ~) by Th15
.= (Flow M) ~ by Th16 ;
A5: ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~) \/ (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) = ((((Flow M) | the carrier' of M) ~) \/ ((((Flow M) ~) | the carrier' of M) ~)) \/ (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) by RELAT_1:23
.= ((((Flow M) | the carrier' of M) ~) \/ ((((Flow M) ~) | the carrier' of M) \/ ((Flow M) | the carrier' of M))) \/ ((((Flow M) ~) | the carrier' of M) ~) by XBOOLE_1:4
.= (((((Flow M) | the carrier' of M) ~) \/ (((Flow M) ~) | the carrier' of M)) \/ ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) ~) by XBOOLE_1:4
.= (Flow M) \/ ((Flow M) ~) by A3, A4, XBOOLE_1:4 ;
A6: (f_adjac M) \/ ((f_adjac M) ~) = ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~) \/ ((id the carrier' of M) ~)) by RELAT_1:23
.= (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~)) \/ ((id the carrier' of M) ~) by XBOOLE_1:4
.= (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~)) \/ (id the carrier' of M)) \/ ((id the carrier' of M) ~) by XBOOLE_1:4
.= ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~)) \/ ((id the carrier' of M) \/ ((id the carrier' of M) ~)) by XBOOLE_1:4
.= ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) ~)) \/ ((id the carrier' of M) \/ (id the carrier' of M))
.= ((Flow M) \/ ((Flow M) ~)) \/ (id the carrier' of M) by A5 ;
A7: id the carrier' of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
A8: (f_adjac M) * (f_adjac M) = (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by RELAT_1:32
.= ((((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * ((Flow M) | the carrier' of M)) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (((Flow M) ~) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by RELAT_1:32
.= ((((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * ((Flow M) | the carrier' of M)) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (((Flow M) ~) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by SYSREL:6
.= ((((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (((Flow M) ~) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by SYSREL:6
.= ((((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (((Flow M) ~) | the carrier' of M)) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by SYSREL:6
.= ((((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (id the carrier' of M)) * (id the carrier' of M)) by SYSREL:6
.= ((((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (id the carrier' of M)) \/ ((id the carrier' of M) * (id the carrier' of M))) by SYSREL:6
.= ((((((Flow M) | the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by SYSREL:6
.= ((({} \/ ((((Flow M) ~) | the carrier' of M) * ((Flow M) | the carrier' of M))) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th11
.= ((({} \/ {}) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (((Flow M) ~) | the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th11
.= ((({} \/ {}) \/ ((id the carrier' of M) * ((Flow M) | the carrier' of M))) \/ (({} \/ ((((Flow M) ~) | the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th11
.= (((id the carrier' of M) * ((Flow M) | the carrier' of M)) \/ ({} \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M)))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th11
.= (((Flow M) | the carrier' of M) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier' of M))) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th12
.= (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ ((id the carrier' of M) * (id the carrier' of M))) by Th12
.= (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (((((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ (id the carrier' of M)) by SYSREL:12
.= (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ (({} \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M))) \/ (id the carrier' of M)) by Th12
.= (((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) \/ ({} \/ (id the carrier' of M)) by Th12
.= f_adjac M ;
A9: ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} \/ ((((Flow M) | the carrier' of M) \/ (((Flow M) ~) | the carrier' of M)) * (id the carrier' of M)) by A1, A2, RELAT_1:32
.= (((Flow M) | the carrier' of M) * (id the carrier' of M)) \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M)) by SYSREL:6
.= {} \/ ((((Flow M) ~) | the carrier' of M) * (id the carrier' of M)) by Th12
.= {} by Th12 ;
((f_adjac M) \/ ((f_adjac M) ~)) \/ (id (Elements M)) = ((Flow M) \/ ((Flow M) ~)) \/ ((id the carrier' of M) \/ (id (Elements M))) by A6, XBOOLE_1:4
.= ((Flow M) \/ ((Flow M) ~)) \/ (id (Elements M)) by A7, XBOOLE_1:12
.= ((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ (id (Elements M))) by XBOOLE_1:5
.= ((Flow M) \/ (id (Elements M))) \/ (((Flow M) ~) \/ ((id (Elements M)) ~))
.= (f_circulation M) \/ ((f_circulation M) ~) by RELAT_1:23 ;
hence  ( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~)) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~) ) by A8, A9; ::_thesis: verum
end;