I am studying the complexity of SAT resolution refutation. There is a useful tool named weakening rule
The weakening rule:
B -->B ∨ C says that from a clause B we can derive the weaker clause B ∨ C for an arbitrary C. We say that B ∨ C is a weakening of B. We can add this extra rule without loss of generality, since any applications of weakening in a resolution refutation can always be eliminated.
My question: Why weakening rule doesn't increase the size of resolution refutation?
where size means the number of clauses the refutation contained.
Ituitively, I can understand it, but I can't state the proof formally.