A1: ( rng (id A) = A & dom (id A) = A ) ;
thus incl is Function of A,Y by A1, FUNCT_2:2; :: thesis: verum