let M be Pnet; :: thesis: ( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )
A1: for x being set st x in dom (f_exit M) holds
x in Elements M

proof

let x be set ; :: thesis: ( x in dom (f_exit M) implies x in Elements M )
assume x in dom (f_exit M) ; :: thesis: x in Elements M
then x in (dom (the Flow of M | the Transitions of M)) \/ (dom (id the Places of M)) by RELAT_1:13;
then ( x in dom (the Flow of M | the Transitions of M) or x in dom (id the Places of M) ) by XBOOLE_0:def 3;
then ( x in the Transitions of M or x in the Places of M ) by RELAT_1:71, RELAT_1:86;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

A2: for x being set st x in rng (f_exit M) holds
x in Elements M

proof

let x be set ; :: thesis: ( x in rng (f_exit M) implies x in Elements M )
assume x in rng (f_exit M) ; :: thesis: x in Elements M
then A3: x in (rng (the Flow of M | the Transitions of M)) \/ (rng (id the Places of M)) by RELAT_1:26;
A4: ( x in rng (the Flow of M | the Transitions of M) implies x in Elements M )

proof

assume x in rng (the Flow of M | the Transitions of M) ; :: thesis: x in Elements 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 in the Transitions of M by A5, RELAT_1:def 11;
[y,x] in the Flow of M by A5, RELAT_1:def 11;
then ( x in the Transitions of M or x in the Places of M ) by A6, Th11;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

( x in rng (id the Places of M) implies x in Elements M )

proof

assume x in rng (id the Places of M) ; :: thesis: x in Elements M
then ( x in the Transitions of M or x in the Places of M ) by RELAT_1:71;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in Elements M by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

A7: for x being set st x in dom (f_enter M) holds
x in Elements M

proof

let x be set ; :: thesis: ( x in dom (f_enter M) implies x in Elements M )
assume x in dom (f_enter M) ; :: thesis: x in Elements M
then x in (dom ((the Flow of M ~ ) | the Transitions of M)) \/ (dom (id the Places of M)) by RELAT_1:13;
then ( x in dom ((the Flow of M ~ ) | the Transitions of M) or x in dom (id the Places of M) ) by XBOOLE_0:def 3;
then ( x in the Transitions of M or x in the Places of M ) by RELAT_1:71, RELAT_1:86;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

for x being set st x in rng (f_enter M) holds
x in Elements M

proof

let x be set ; :: thesis: ( x in rng (f_enter M) implies x in Elements M )
assume x in rng (f_enter M) ; :: thesis: x in Elements M
then A8: x in (rng ((the Flow of M ~ ) | the Transitions of M)) \/ (rng (id the Places of M)) by RELAT_1:26;
A9: ( x in rng ((the Flow of M ~ ) | the Transitions of M) implies x in Elements M )

proof

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

end;

( x in rng (id the Places of M) implies x in Elements M )

proof

assume x in rng (id the Places of M) ; :: thesis: x in Elements M
then ( x in the Transitions of M or x in the Places of M ) by RELAT_1:71;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

hence x in Elements M by A8, A9, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M ) by A1, A2, A7, TARSKI:def 3; :: thesis: verum