We study the proof complexity of Bonattiś and Olivettiś formalization of propositional default logic. we show that, depending on the kind of reasoning (credulous and skeptical), proofs in their system are as long as classical propositional logic ( thus the formalization cannot be improved) or of exponential size, respectively.