let M be Pnet; ( (the Flow of M | the Places of M) ~ = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Transitions of M) ~ = (the Flow of M ~ ) | the Places of M )
set R = the Flow of M;
set X = the Places of M;
set Y = the Transitions of M;
for x, y being set st [x,y] in (the Flow of M | the Places of M) ~ holds
[x,y] in (the Flow of M ~ ) | the Transitions of M
proof
let x,
y be
set ;
( [x,y] in (the Flow of M | the Places of M) ~ implies [x,y] in (the Flow of M ~ ) | the Transitions of M )
assume
[x,y] in (the Flow of M | the Places of M) ~
;
[x,y] in (the Flow of M ~ ) | the Transitions of M
then A1:
[y,x] in the
Flow of
M | the
Places of
M
by RELAT_1:def 7;
then A2:
[y,x] in the
Flow of
M
by RELAT_1:def 11;
A3:
y in the
Places of
M
by A1, RELAT_1:def 11;
A4:
[x,y] in the
Flow of
M ~
by A2, RELAT_1:def 7;
x in the
Transitions of
M
by A2, A3, Th11;
hence
[x,y] in (the Flow of M ~ ) | the
Transitions of
M
by A4, RELAT_1:def 11;
verum
end;
then A5:
(the Flow of M | the Places of M) ~ c= (the Flow of M ~ ) | the Transitions of M
by RELAT_1:def 3;
for x, y being set st [x,y] in (the Flow of M ~ ) | the Transitions of M holds
[x,y] in (the Flow of M | the Places of M) ~
proof
let x,
y be
set ;
( [x,y] in (the Flow of M ~ ) | the Transitions of M implies [x,y] in (the Flow of M | the Places of M) ~ )
assume A6:
[x,y] in (the Flow of M ~ ) | the
Transitions of
M
;
[x,y] in (the Flow of M | the Places of M) ~
then
[x,y] in the
Flow of
M ~
by RELAT_1:def 11;
then A7:
[y,x] in the
Flow of
M
by RELAT_1:def 7;
x in the
Transitions of
M
by A6, RELAT_1:def 11;
then
y in the
Places of
M
by A7, Th11;
then
[y,x] in the
Flow of
M | the
Places of
M
by A7, RELAT_1:def 11;
hence
[x,y] in (the Flow of M | the Places of M) ~
by RELAT_1:def 7;
verum
end;
then A8:
(the Flow of M ~ ) | the Transitions of M c= (the Flow of M | the Places of M) ~
by RELAT_1:def 3;
for x, y being set st [x,y] in (the Flow of M | the Transitions of M) ~ holds
[x,y] in (the Flow of M ~ ) | the Places of M
proof
let x,
y be
set ;
( [x,y] in (the Flow of M | the Transitions of M) ~ implies [x,y] in (the Flow of M ~ ) | the Places of M )
assume
[x,y] in (the Flow of M | the Transitions of M) ~
;
[x,y] in (the Flow of M ~ ) | the Places of M
then A9:
[y,x] in the
Flow of
M | the
Transitions of
M
by RELAT_1:def 7;
then A10:
[y,x] in the
Flow of
M
by RELAT_1:def 11;
A11:
y in the
Transitions of
M
by A9, RELAT_1:def 11;
A12:
[x,y] in the
Flow of
M ~
by A10, RELAT_1:def 7;
x in the
Places of
M
by A10, A11, Th11;
hence
[x,y] in (the Flow of M ~ ) | the
Places of
M
by A12, RELAT_1:def 11;
verum
end;
then A13:
(the Flow of M | the Transitions of M) ~ c= (the Flow of M ~ ) | the Places of M
by RELAT_1:def 3;
for x, y being set st [x,y] in (the Flow of M ~ ) | the Places of M holds
[x,y] in (the Flow of M | the Transitions of M) ~
proof
let x,
y be
set ;
( [x,y] in (the Flow of M ~ ) | the Places of M implies [x,y] in (the Flow of M | the Transitions of M) ~ )
assume A14:
[x,y] in (the Flow of M ~ ) | the
Places of
M
;
[x,y] in (the Flow of M | the Transitions of M) ~
then
[x,y] in the
Flow of
M ~
by RELAT_1:def 11;
then A15:
[y,x] in the
Flow of
M
by RELAT_1:def 7;
x in the
Places of
M
by A14, RELAT_1:def 11;
then
y in the
Transitions of
M
by A15, Th11;
then
[y,x] in the
Flow of
M | the
Transitions of
M
by A15, RELAT_1:def 11;
hence
[x,y] in (the Flow of M | the Transitions of M) ~
by RELAT_1:def 7;
verum
end;
then
(the Flow of M ~ ) | the Places of M c= (the Flow of M | the Transitions of M) ~
by RELAT_1:def 3;
hence
( (the Flow of M | the Places of M) ~ = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Transitions of M) ~ = (the Flow of M ~ ) | the Places of M )
by A5, A8, A13, XBOOLE_0:def 10; verum