reconsider f = id (bool A) as Function of (bool A),(bool A) ;
{} c= A ;
then A1: f . {} = {} by FUNCT_1:18;
A in bool A by ZFMISC_1:def 1;
then f . A = A by FUNCT_1:18;
hence for b₁ being Function of (bool A),(bool A) st b₁ = id (bool A) holds
( b₁ is empty-preserving & b₁ is universe-preserving ) by A1; :: thesis: verum