let M be Pnet; :: thesis: ( (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;
A1:
(the Flow of M | the Places of M) ~ c= (the Flow of M ~ ) | the Transitions of M
proof
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 ;
:: thesis: ( [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) ~
;
:: thesis: [x,y] in (the Flow of M ~ ) | the Transitions of M
then
[y,x] in the
Flow of
M | the
Places of
M
by RELAT_1:def 7;
then
(
[y,x] in the
Flow of
M &
y in the
Places of
M )
by RELAT_1:def 11;
then
(
[x,y] in the
Flow of
M ~ &
x in the
Transitions of
M )
by Th11, RELAT_1:def 7;
hence
[x,y] in (the Flow of M ~ ) | the
Transitions of
M
by RELAT_1:def 11;
:: thesis: verum
end;
hence
(the Flow of M | the Places of M) ~ c= (the Flow of M ~ ) | the
Transitions of
M
by RELAT_1:def 3;
:: thesis: verum
end;
A2:
(the Flow of M ~ ) | the Transitions of M c= (the Flow of M | the Places of M) ~
proof
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 ;
:: thesis: ( [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
;
:: thesis: [x,y] in (the Flow of M | the Places of M) ~
then
(
[x,y] in the
Flow of
M ~ &
x in the
Transitions of
M )
by RELAT_1:def 11;
then
(
[y,x] in the
Flow of
M &
x in the
Transitions of
M )
by RELAT_1:def 7;
then
(
[y,x] in the
Flow of
M &
y in the
Places of
M )
by Th11;
then
[y,x] in the
Flow of
M | the
Places of
M
by RELAT_1:def 11;
hence
[x,y] in (the Flow of M | the Places of M) ~
by RELAT_1:def 7;
:: thesis: verum
end;
hence
(the Flow of M ~ ) | the
Transitions of
M c= (the Flow of M | the Places of M) ~
by RELAT_1:def 3;
:: thesis: verum
end;
A3:
(the Flow of M | the Transitions of M) ~ c= (the Flow of M ~ ) | the Places of M
proof
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 ;
:: thesis: ( [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) ~
;
:: thesis: [x,y] in (the Flow of M ~ ) | the Places of M
then
[y,x] in the
Flow of
M | the
Transitions of
M
by RELAT_1:def 7;
then
(
[y,x] in the
Flow of
M &
y in the
Transitions of
M )
by RELAT_1:def 11;
then
(
[x,y] in the
Flow of
M ~ &
x in the
Places of
M )
by Th11, RELAT_1:def 7;
hence
[x,y] in (the Flow of M ~ ) | the
Places of
M
by RELAT_1:def 11;
:: thesis: verum
end;
hence
(the Flow of M | the Transitions of M) ~ c= (the Flow of M ~ ) | the
Places of
M
by RELAT_1:def 3;
:: thesis: verum
end;
(the Flow of M ~ ) | the Places of M c= (the Flow of M | the Transitions of M) ~
proof
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 ;
:: thesis: ( [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
;
:: thesis: [x,y] in (the Flow of M | the Transitions of M) ~
then
(
[x,y] in the
Flow of
M ~ &
x in the
Places of
M )
by RELAT_1:def 11;
then
(
[y,x] in the
Flow of
M &
x in the
Places of
M )
by RELAT_1:def 7;
then
(
[y,x] in the
Flow of
M &
y in the
Transitions of
M )
by Th11;
then
[y,x] in the
Flow of
M | the
Transitions of
M
by RELAT_1:def 11;
hence
[x,y] in (the Flow of M | the Transitions of M) ~
by RELAT_1:def 7;
:: thesis: verum
end;
hence
(the Flow of M ~ ) | the
Places of
M c= (the Flow of M | the Transitions of M) ~
by RELAT_1:def 3;
:: thesis: verum
end;
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 A1, A2, A3, XBOOLE_0:def 10; :: thesis: verum