The closed unit ball of the double dual of a Banach space is weak* compact. This theorem is equivalent to the Tychonoff theorem for compactHausdorffspaces (eg Rossi 2009), and as such is not constructive in general. However, the restriction of the statement to separable Banach spaces is constructive, and is used in PDE theory to find solutions. A constructive proof can be found e.g. in BridgesVita.