A1: ( rng (id A) = A & dom (id A) = A ) by RELAT_1:45;
( Y = {} implies A = {} ) ;
hence incl is Function of A,Y by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum