A Note on Formalizing Undefined Terms in Real Analysis