I don’t necessarily agree that the second theorem should not be a separate theorem. The first theorem just states that a unique functional exists, not how it should look like or the features it should have. I do agree that intuitively we can expect that the functional reaches a minimum for the ground state density, because nature wants to minimise (free) energy.