let M be Pnet; :: thesis: ( rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (id the Places of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (id the Places of M) & rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M) & rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng (the Flow of M | the Places of M) misses dom (id the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) & dom (the Flow of M | the Places of M) misses rng (the Flow of M | the Places of M) & dom (the Flow of M | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (the Flow of M | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) )
set R = the Flow of M | the Transitions of M;
set S = (the Flow of M ~ ) | the Transitions of M;
set T = id the Transitions of M;
set R1 = the Flow of M | the Places of M;
set S1 = (the Flow of M ~ ) | the Places of M;
set T1 = id the Places of M;
A1: dom (the Flow of M | the Transitions of M) c= the Transitions of M by RELAT_1:87;
A2: rng (the Flow of M | the Transitions of M) c= the Places of M by Th14;
A3: dom ((the Flow of M ~ ) | the Transitions of M) c= the Transitions of M by RELAT_1:87;
A4: rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M by Th14;
A5: dom (id the Transitions of M) c= the Transitions of M by Th14;
A6: rng (id the Transitions of M) c= the Transitions of M by Th14;
A7: dom (the Flow of M | the Places of M) c= the Places of M by RELAT_1:87;
A8: rng (the Flow of M | the Places of M) c= the Transitions of M by Th14;
A9: dom ((the Flow of M ~ ) | the Places of M) c= the Places of M by RELAT_1:87;
A10: rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M by Th14;
A11: dom (id the Places of M) c= the Places of M by Th14;
A12: rng (id the Places of M) c= the Places of M by Th14;
the Places of M misses the Transitions of M by NET_1:def 1;
hence ( rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (id the Places of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (id the Places of M) & rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M) & rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng (the Flow of M | the Places of M) misses dom (id the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) & dom (the Flow of M | the Places of M) misses rng (the Flow of M | the Places of M) & dom (the Flow of M | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (the Flow of M | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) ) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, Lm1; :: thesis: verum