Theorem

Name: Urysohn implies Comp. Hausdorff
Hypothesis: Urysohn
Conclusion: Completely Hausdorff
Human Entered Proof: Fix [tex]a, b \in X[/tex]. Let [tex]f: X \to [0,1][/tex] be a continuous function such that [tex]f(a) = 1[/tex] and [tex]f(b) = 0[/tex]. Let [tex]U_a = f^{-1}((3/4,1])[/tex] and [tex]U_b = f^{-1}([0,1/4))[/tex]. [tex]U_a[/tex] and [tex]U_b[/tex] are disjoint open sets containing [tex]a[/tex] and [tex]b[/tex] respectively.

Note: This selection of hypothesis and conclusion is only one way to interpret this theorem. The theorem could be written as many different logically equivalent implications.