Description: Define base set of Hilbert space, for use if we want to develop Hilbert
space independently from the axioms (see comments in ax-hilex ). Note
that ~H is considered a primitive in the Hilbert space axioms below,
and we don't use this definition outside of this section. This definition
can be proved independently from those axioms as Theorem hhba .
(Contributed by NM, 31-May-2008)(New usage is discouraged.)