A theorem from Herrlich and Strecker

A theorem from Herrlich and Strecker

[Pierre Cardascia]

Dear Catégoristes,

I'm working on an introduction for categorical logic, and I try to avoid using the notion of limit before introducing the notion of functor in my work (because limit means limit of functors. Squarely, we can introduce the limit before, but we don't understand why the limit is called limit, and limit of what ??).
But I have to introduce the notion of categories finitely complete. SO I think about this theorem :
===> If C has a terminal object, and a pullback for each pair of arrows with common codomains, then C is finitively complete.
I found that without any proof in Goldblatt. Rob Goldblatt just said : "you can find it into such book from Herrlich and Strecker"... Does somebody has the proof ? Can I use this theorem to define complety closed categories instead of working with limits ? Or does somebody have any way to define complety closed categories without any reference to functors ?

Thanks !

Pierre CARDASCIA