let R be Relation; :: thesis: ( ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) & ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R ) )
thus ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) :: thesis: ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R )

proof

assume that
A1: R c= R * R and
A2: R * (R \ (id (rng R))) = {} ; :: thesis: id (rng R) c= R
for y being object st y in rng R holds
[y,y] in R

proof

let y be object ; :: thesis: ( y in rng R implies [y,y] in R )
assume y in rng R ; :: thesis: [y,y] in R
then consider x being object such that
A3: [x,y] in R by XTUPLE_0:def 13;
consider z being object such that
A4: [x,z] in R and
A5: [z,y] in R by A1, A3, RELAT_1:def 8;
z = y

proof

assume z <> y ; :: thesis: contradiction
then not [z,y] in id (rng R) by RELAT_1:def 10;
then [z,y] in R \ (id (rng R)) by A5, XBOOLE_0:def 5;
hence contradiction by A2, A4, RELAT_1:def 8; :: thesis: verum

end;

hence [y,y] in R by A5; :: thesis: verum

end;

hence id (rng R) c= R by RELAT_1:47; :: thesis: verum

end;

assume that
A6: R c= R * R and
A7: (R \ (id (dom R))) * R = {} ; :: thesis: id (dom R) c= R
for x being object st x in dom R holds
[x,x] in R

proof

let x be object ; :: thesis: ( x in dom R implies [x,x] in R )
assume x in dom R ; :: thesis: [x,x] in R
then consider y being object such that
A8: [x,y] in R by XTUPLE_0:def 12;
consider z being object such that
A9: [x,z] in R and
A10: [z,y] in R by A6, A8, RELAT_1:def 8;
z = x

proof

assume z <> x ; :: thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def 10;
then [x,z] in R \ (id (dom R)) by A9, XBOOLE_0:def 5;
hence contradiction by A7, A10, RELAT_1:def 8; :: thesis: verum

end;

hence [x,x] in R by A9; :: thesis: verum

end;

hence id (dom R) c= R by RELAT_1:47; :: thesis: verum