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