thus rng (id X) c= X :: according to XBOOLE_0:def 10 :: thesis: X c= rng (id X)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (id X) or x in X )
assume x in rng (id X) ; :: thesis: x in X
then consider y being object such that
A1: [y,x] in id X by XTUPLE_0:def 13;
x = y by A1, Def8;
hence x in X by A1, Def8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in rng (id X) )
( [x,x] in id X iff x in X ) by Def8;
hence ( not x in X or x in rng (id X) ) by XTUPLE_0:def 13; :: thesis: verum