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 object st x in dom (f_exit M) holds
x in Elements M

proof

let x be object ; :: 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 ((Flow M) | the carrier' of M)) \/ (dom (id the carrier of M)) by XTUPLE_0:23;
then ( x in dom ((Flow M) | the carrier' of M) or x in dom (id the carrier of M) ) by XBOOLE_0:def 3;
then ( x in the carrier' of M or x in the carrier of M ) by RELAT_1:57;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let x be object ; :: 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 ((Flow M) | the carrier' of M)) \/ (rng (id the carrier of M)) by RELAT_1:12;
A4: ( x in rng ((Flow M) | the carrier' of M) implies x in Elements M )

proof

assume x in rng ((Flow M) | the carrier' of M) ; :: thesis: x in Elements M
then consider y being object such that
A5: [y,x] in (Flow M) | the carrier' of M by XTUPLE_0:def 13;
A6: y in the carrier' of M by A5, RELAT_1:def 11;
[y,x] in Flow M by A5, RELAT_1:def 11;
then ( x in the carrier' of M or x in the carrier of M ) by A6, Th7;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

( x in rng (id the carrier of M) implies x in Elements M ) by XBOOLE_0:def 3;
hence x in Elements M by A3, A4, XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let x be object ; :: 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 (((Flow M) ~) | the carrier' of M)) \/ (dom (id the carrier of M)) by XTUPLE_0:23;
then ( x in dom (((Flow M) ~) | the carrier' of M) or x in dom (id the carrier of M) ) by XBOOLE_0:def 3;
then ( x in the carrier' of M or x in the carrier of M ) by RELAT_1:57;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

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

proof

let x be object ; :: 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 (((Flow M) ~) | the carrier' of M)) \/ (rng (id the carrier of M)) by RELAT_1:12;
A9: ( x in rng (((Flow M) ~) | the carrier' of M) implies x in Elements M )

proof

assume x in rng (((Flow M) ~) | the carrier' of M) ; :: thesis: x in Elements M
then consider y being object such that
A10: [y,x] in ((Flow M) ~) | the carrier' of M by XTUPLE_0:def 13;
A11: [y,x] in (Flow M) ~ by A10, RELAT_1:def 11;
A12: y in the carrier' of M by A10, RELAT_1:def 11;
[x,y] in Flow M by A11, RELAT_1:def 7;
then ( x in the carrier' of M or x in the carrier of M ) by A12, Th7;
hence x in Elements M by XBOOLE_0:def 3; :: thesis: verum

end;

( x in rng (id the carrier of M) implies x in Elements M ) by XBOOLE_0:def 3;
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