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 object st [x,y] in ((Flow M) | the carrier of M) ~ holds

[x,y] in ((Flow M) ~) | 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) ~

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

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) ~

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

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

then A5:
((Flow M) | the carrier of M) ~ c= ((Flow M) ~) | the carrier' of M
by RELAT_1:def 3;
let x, y be object ; :: 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;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

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

then A8:
((Flow M) ~) | the carrier' of M c= ((Flow M) | the carrier of M) ~
by RELAT_1:def 3;
let x, y be object ; :: 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;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

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

then A13:
((Flow M) | the carrier' of M) ~ c= ((Flow M) ~) | the carrier of M
by RELAT_1:def 3;
let x, y be object ; :: 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;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

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

then
((Flow M) ~) | the carrier of M c= ((Flow M) | the carrier' of M) ~
by RELAT_1:def 3;
let x, y be object ; :: 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;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

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