reconsider f = id (bool A) as Function of (bool A),(bool A) ;
( f is empty-preserving & f is universe-preserving ) ;
hence ex b₁ being Function of (bool A),(bool A) st
( b₁ is empty-preserving & b₁ is universe-preserving ) ; :: thesis: verum