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

x in Elements M

x in Elements M

x in Elements M

A1: for x being object st x in dom (f_exit M) holds

x in Elements M

proof

A2:
for x being object st x in rng (f_exit M) holds
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;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

x in Elements M

proof

A7:
for x being object st x in dom (f_enter M) holds
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 )

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

end;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

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

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

x in Elements M

proof

for x being object st x in rng (f_enter M) holds
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;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

x in Elements M

proof

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
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 )

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

end;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

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

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