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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (id X) or x in X )
assume x in dom (id X) ; :: thesis: x in X
then ex y being object st [x,y] in id X by XTUPLE_0:def 12;
hence x in X by Def8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in dom (id X) )
assume x in X ; :: thesis: x in dom (id X)
then [x,x] in id X by Def8;
hence x in dom (id X) by XTUPLE_0:def 12; :: thesis: verum