take EnsCat {{}} ; :: thesis: EnsCat {{}} is with_products
thus EnsCat {{}} is with_products ; :: thesis: verum