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 ;
A4: [x,y] in (Flow M) ~ by ;
x in the carrier' of M by A2, A3, Th7;
hence [x,y] in ((Flow M) ~) | the carrier' of M by ; :: 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 ;
then y in the carrier of M by ;
then [y,x] in (Flow M) | the carrier of M by ;
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 ;
A12: [x,y] in (Flow M) ~ by ;
x in the carrier of M by ;
hence [x,y] in ((Flow M) ~) | the carrier of M by ; :: 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 ;
then y in the carrier' of M by ;
then [y,x] in (Flow M) | the carrier' of M by ;
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 ; :: thesis: verum