let M be Pnet; ( (the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * ((the Flow of M ~ ) | the Transitions 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) * (the Flow of M | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M) = {} )
A1:
rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M)
by Th15;
A2:
rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M)
by Th15;
A3:
rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M)
by Th15;
A4:
rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M)
by Th15;
A5:
rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M)
by Th15;
A6:
rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M)
by Th15;
A7:
rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M)
by Th15;
rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M)
by Th15;
hence
( (the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * ((the Flow of M ~ ) | the Transitions 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) * (the Flow of M | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M) = {} )
by A1, A2, A3, A4, A5, A6, A7, RELAT_1:67; verum