let M be Pnet; ( ((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 object 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
object ;
( [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) ~
;
[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;
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 object 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
object ;
( [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
;
[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;
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 object 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
object ;
( [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) ~
;
[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;
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 object 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
object ;
( [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
;
[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;
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; verum