let X be set ; :: thesis: id X is Relation of X
( dom (id X) c= X & rng (id X) c= X ) by RELAT_1:71;
hence id X is Relation of X by RELSET_1:11; :: thesis: verum