Вопрос по мат логике.

Правило контр позиции может быть применено к одной скобке/части формулы?
Есть такая формула ((-[X v Y] -> -Y) -> (-[X v Y] -> -X & -Y)).
Как я понимаю рассматривается избавление/выводимость (-[X v Y] -> -Y)
Берется аксиома (x -> y) -> (-y -> -x)
и производится подстановка x на у, y на x v y и получаем:
(Y -> X v Y) -> (-[X v Y] -> -Y) и далее из этого как-то выходит:
(-[X v Y] -> -Y) -> (-[X v Y] -> -Y) Вот это мне и интересно. Похоже на применение правила контрпозиции или как это получено?

квадратные скобки использовал, чтобы показать отрицание над всем выражением что в скобках