Cartesian closed category

definiendum	${\bf C}$ in it
inclusion	${\bf C}$ … category
postulate	${\bf C}$ has a terminal object
postulate	For all $X,Y\in{\bf C}$ , the product $X\times Y$ exists
postulate	For all $Y\in{\bf C}$ , the functor $-\times Y$ from ${\bf C}$ to ${\bf C}$ has a right adjoint

Remark/Reminder:

$((A\times Y)\to B)\cong(A\to B^Y)$