В этом докладе мы обсудим детали доказательства нижней оценки на систему доказательств AC_0-Frege. Нашей основной целью будет разобраться в технических деталях switching леммы для паросочетаний из классической статьи Urquhart, Fu ``Simplified Lower Bounds for Propositional Proofs''.