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

proof

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;

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 ; :: 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 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 ; :: 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 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 ; :: 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