let M be Pnet; :: thesis: ( rng (the Flow of M | the Transitions of M) c= the Places of M & rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M & rng (the Flow of M | the Places of M) c= the Transitions of M & rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M & rng (id the Transitions of M) c= the Transitions of M & dom (id the Transitions of M) c= the Transitions of M & rng (id the Places of M) c= the Places of M & dom (id the Places of M) c= the Places of M )
A1: for x being set st x in rng (the Flow of M | the Transitions of M) holds
x in the Places of M

proof

let x be set ; :: thesis: ( x in rng (the Flow of M | the Transitions of M) implies x in the Places of M )
assume x in rng (the Flow of M | the Transitions of M) ; :: thesis: x in the Places of M
then consider y being set such that
A2: [y,x] in the Flow of M | the Transitions of M by RELAT_1:def 5;
A3: y in the Transitions of M by A2, RELAT_1:def 11;
[y,x] in the Flow of M by A2, RELAT_1:def 11;
hence x in the Places of M by A3, Th11; :: thesis: verum

end;

A4: for x being set st x in rng ((the Flow of M ~ ) | the Transitions of M) holds
x in the Places of M

proof

let x be set ; :: thesis: ( x in rng ((the Flow of M ~ ) | the Transitions of M) implies x in the Places of M )
assume x in rng ((the Flow of M ~ ) | the Transitions of M) ; :: thesis: x in the Places of M
then consider y being set such that
A5: [y,x] in (the Flow of M ~ ) | the Transitions of M by RELAT_1:def 5;
A6: [y,x] in the Flow of M ~ by A5, RELAT_1:def 11;
A7: y in the Transitions of M by A5, RELAT_1:def 11;
[x,y] in the Flow of M by A6, RELAT_1:def 7;
hence x in the Places of M by A7, Th11; :: thesis: verum

end;

A8: for x being set st x in rng (the Flow of M | the Places of M) holds
x in the Transitions of M

proof

let x be set ; :: thesis: ( x in rng (the Flow of M | the Places of M) implies x in the Transitions of M )
assume x in rng (the Flow of M | the Places of M) ; :: thesis: x in the Transitions of M
then consider y being set such that
A9: [y,x] in the Flow of M | the Places of M by RELAT_1:def 5;
A10: y in the Places of M by A9, RELAT_1:def 11;
[y,x] in the Flow of M by A9, RELAT_1:def 11;
hence x in the Transitions of M by A10, Th11; :: thesis: verum

end;

for x being set st x in rng ((the Flow of M ~ ) | the Places of M) holds
x in the Transitions of M

proof

let x be set ; :: thesis: ( x in rng ((the Flow of M ~ ) | the Places of M) implies x in the Transitions of M )
assume x in rng ((the Flow of M ~ ) | the Places of M) ; :: thesis: x in the Transitions of M
then consider y being set such that
A11: [y,x] in (the Flow of M ~ ) | the Places of M by RELAT_1:def 5;
A12: [y,x] in the Flow of M ~ by A11, RELAT_1:def 11;
A13: y in the Places of M by A11, RELAT_1:def 11;
[x,y] in the Flow of M by A12, RELAT_1:def 7;
hence x in the Transitions of M by A13, Th11; :: thesis: verum

end;

hence ( rng (the Flow of M | the Transitions of M) c= the Places of M & rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M & rng (the Flow of M | the Places of M) c= the Transitions of M & rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M & rng (id the Transitions of M) c= the Transitions of M & dom (id the Transitions of M) c= the Transitions of M & rng (id the Places of M) c= the Places of M & dom (id the Places of M) c= the Places of M ) by A1, A4, A8, RELAT_1:71, TARSKI:def 3; :: thesis: verum