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