let M be Pnet; :: thesis: ( dom () c= Elements M & rng () c= Elements M & dom () c= Elements M & rng () c= Elements M )
A1: for x being object st x in dom () holds
x in Elements M
proof
let x be object ; :: thesis: ( x in dom () implies x in Elements M )
assume x in dom () ; :: thesis:
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 () holds
x in Elements M
proof
let x be object ; :: thesis: ( x in rng () implies x in Elements M )
assume x in rng () ; :: thesis:
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:
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 ;
[y,x] in Flow M by ;
then ( x in the carrier of M or x in the carrier' of M ) by ;
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 ; :: thesis: verum
end;
A7: for x being object st x in dom () holds
x in Elements M
proof
let x be object ; :: thesis: ( x in dom () implies x in Elements M )
assume x in dom () ; :: thesis:
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 () holds
x in Elements M
proof
let x be object ; :: thesis: ( x in rng () implies x in Elements M )
assume x in rng () ; :: thesis:
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:
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 ;
A12: y in the carrier of M by ;
[x,y] in Flow M by ;
then ( x in the carrier of M or x in the carrier' of M ) by ;
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 ; :: thesis: verum
end;
hence ( dom () c= Elements M & rng () c= Elements M & dom () c= Elements M & rng () c= Elements M ) by ; :: thesis: verum