В первой скобке, как я поняла, эквиваленция.
Сначала расписываем следование на дизъюнкцию и конъюнкцию (X -> Y) == (not X v Y)
То есть, not(not[not A <-> B] v (B v A) == (not A <-> B) v A v B
Далее - эквиваленция. (X <-> Y) == (not X v Y)(not Y v X).
То есть, (A v B)(not A v not B) v A v B == A * not B v B * not A v A v B == A v (A * not B) v B v (B * not A) по формулам поглощения получаем == A v B.