Description: Derive axiom ax-his4 from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)