I'd say that the proof of the four-colour theorem (particularly the "first generation" proof of Appel and Haken) is explanatory (we see that the source of four-colourability is the presence of unavoidable subconfigurations in any planar graph which are all reducible, in that the four-colourability of any planar graph containing such a configuration can be deduced from the four-colourability of a smaller graph) but not beautiful. (See for instance the Notices article at http://www.ams.org/notices/199807/thomas.pdf for a description of the proof strategy.)