let M be Pnet; ( (the Flow of M ~ ) | the Transitions of M misses id (Elements M) & the Flow of M | the Transitions of M misses id (Elements M) & (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )
set T = id (Elements M);
thus
(the Flow of M ~ ) | the Transitions of M misses id (Elements M)
( the Flow of M | the Transitions of M misses id (Elements M) & (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )proof
set R =
(the Flow of M ~ ) | the
Transitions of
M;
for
x,
y being
set holds not
[x,y] in ((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M))
proof
let x,
y be
set ;
not [x,y] in ((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M))
assume A1:
[x,y] in ((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M))
;
contradiction
then A2:
[x,y] in (the Flow of M ~ ) | the
Transitions of
M
by XBOOLE_0:def 4;
A3:
[x,y] in id (Elements M)
by A1, XBOOLE_0:def 4;
A4:
[x,y] in the
Flow of
M ~
by A2, RELAT_1:def 11;
A5:
x in the
Transitions of
M
by A2, RELAT_1:def 11;
[y,x] in the
Flow of
M
by A4, RELAT_1:def 7;
then
x <> y
by A5, Th11;
hence
contradiction
by A3, RELAT_1:def 10;
verum
end;
then
((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M)) = {}
by RELAT_1:56;
hence
(the Flow of M ~ ) | the
Transitions of
M misses id (Elements M)
by XBOOLE_0:def 7;
verum
end;
thus
the Flow of M | the Transitions of M misses id (Elements M)
( (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )proof
set R = the
Flow of
M | the
Transitions of
M;
for
x,
y being
set holds not
[x,y] in (the Flow of M | the Transitions of M) /\ (id (Elements M))
proof
let x,
y be
set ;
not [x,y] in (the Flow of M | the Transitions of M) /\ (id (Elements M))
assume A6:
[x,y] in (the Flow of M | the Transitions of M) /\ (id (Elements M))
;
contradiction
then A7:
[x,y] in the
Flow of
M | the
Transitions of
M
by XBOOLE_0:def 4;
A8:
[x,y] in id (Elements M)
by A6, XBOOLE_0:def 4;
A9:
x in the
Transitions of
M
by A7, RELAT_1:def 11;
[x,y] in the
Flow of
M
by A7, RELAT_1:def 11;
then
x <> y
by A9, Th11;
hence
contradiction
by A8, RELAT_1:def 10;
verum
end;
then
(the Flow of M | the Transitions of M) /\ (id (Elements M)) = {}
by RELAT_1:56;
hence
the
Flow of
M | the
Transitions of
M misses id (Elements M)
by XBOOLE_0:def 7;
verum
end;
thus
(the Flow of M ~ ) | the Places of M misses id (Elements M)
the Flow of M | the Places of M misses id (Elements M)proof
set R =
(the Flow of M ~ ) | the
Places of
M;
for
x,
y being
set holds not
[x,y] in ((the Flow of M ~ ) | the Places of M) /\ (id (Elements M))
proof
let x,
y be
set ;
not [x,y] in ((the Flow of M ~ ) | the Places of M) /\ (id (Elements M))
assume A10:
[x,y] in ((the Flow of M ~ ) | the Places of M) /\ (id (Elements M))
;
contradiction
then A11:
[x,y] in (the Flow of M ~ ) | the
Places of
M
by XBOOLE_0:def 4;
A12:
[x,y] in id (Elements M)
by A10, XBOOLE_0:def 4;
A13:
[x,y] in the
Flow of
M ~
by A11, RELAT_1:def 11;
A14:
x in the
Places of
M
by A11, RELAT_1:def 11;
[y,x] in the
Flow of
M
by A13, RELAT_1:def 7;
then
x <> y
by A14, Th11;
hence
contradiction
by A12, RELAT_1:def 10;
verum
end;
then
((the Flow of M ~ ) | the Places of M) /\ (id (Elements M)) = {}
by RELAT_1:56;
hence
(the Flow of M ~ ) | the
Places of
M misses id (Elements M)
by XBOOLE_0:def 7;
verum
end;
set R = the Flow of M | the Places of M;
for x, y being set holds not [x,y] in (the Flow of M | the Places of M) /\ (id (Elements M))
proof
let x,
y be
set ;
not [x,y] in (the Flow of M | the Places of M) /\ (id (Elements M))
assume A15:
[x,y] in (the Flow of M | the Places of M) /\ (id (Elements M))
;
contradiction
then A16:
[x,y] in the
Flow of
M | the
Places of
M
by XBOOLE_0:def 4;
A17:
[x,y] in id (Elements M)
by A15, XBOOLE_0:def 4;
A18:
x in the
Places of
M
by A16, RELAT_1:def 11;
[x,y] in the
Flow of
M
by A16, RELAT_1:def 11;
then
x <> y
by A18, Th11;
hence
contradiction
by A17, RELAT_1:def 10;
verum
end;
then
(the Flow of M | the Places of M) /\ (id (Elements M)) = {}
by RELAT_1:56;
hence
the Flow of M | the Places of M misses id (Elements M)
by XBOOLE_0:def 7; verum