let M be Pnet; :: thesis: ( (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) :: thesis: ( 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 ; :: thesis: not [x,y] in ((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M))
assume [x,y] in ((the Flow of M ~ ) | the Transitions of M) /\ (id (Elements M)) ; :: thesis: contradiction
then A1: ( [x,y] in (the Flow of M ~ ) | the Transitions of M & [x,y] in id (Elements M) ) by XBOOLE_0:def 4;
then ( x in the Transitions of M & [x,y] in the Flow of M ~ ) by RELAT_1:def 11;
then ( x in the Transitions of M & [y,x] in the Flow of M ) by RELAT_1:def 7;
then x <> y by Th11;
hence contradiction by A1, RELAT_1:def 10; :: thesis: 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; :: thesis: verum

end;

thus the Flow of M | the Transitions of M misses id (Elements M) :: thesis: ( (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 ; :: thesis: not [x,y] in (the Flow of M | the Transitions of M) /\ (id (Elements M))
assume [x,y] in (the Flow of M | the Transitions of M) /\ (id (Elements M)) ; :: thesis: contradiction
then A2: ( [x,y] in the Flow of M | the Transitions of M & [x,y] in id (Elements M) ) by XBOOLE_0:def 4;
then ( x in the Transitions of M & [x,y] in the Flow of M ) by RELAT_1:def 11;
then x <> y by Th11;
hence contradiction by A2, RELAT_1:def 10; :: thesis: 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; :: thesis: verum

end;

thus (the Flow of M ~ ) | the Places of M misses id (Elements M) :: thesis: 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 ; :: thesis: not [x,y] in ((the Flow of M ~ ) | the Places of M) /\ (id (Elements M))
assume [x,y] in ((the Flow of M ~ ) | the Places of M) /\ (id (Elements M)) ; :: thesis: contradiction
then A3: ( [x,y] in (the Flow of M ~ ) | the Places of M & [x,y] in id (Elements M) ) by XBOOLE_0:def 4;
then ( x in the Places of M & [x,y] in the Flow of M ~ ) by RELAT_1:def 11;
then ( x in the Places of M & [y,x] in the Flow of M ) by RELAT_1:def 7;
then x <> y by Th11;
hence contradiction by A3, RELAT_1:def 10; :: thesis: 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; :: thesis: 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 ; :: thesis: not [x,y] in (the Flow of M | the Places of M) /\ (id (Elements M))
assume [x,y] in (the Flow of M | the Places of M) /\ (id (Elements M)) ; :: thesis: contradiction
then A4: ( [x,y] in the Flow of M | the Places of M & [x,y] in id (Elements M) ) by XBOOLE_0:def 4;
then ( x in the Places of M & [x,y] in the Flow of M ) by RELAT_1:def 11;
then x <> y by Th11;
hence contradiction by A4, RELAT_1:def 10; :: thesis: 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; :: thesis: verum