1,　(a^2≦2b)　∨　(2b≧0　∧　|a|<0)　・・・仮定
2,　(2b≧0　∧　|a|<0)　・・・・・・・・・・1の後の選言肢を仮定
3,　|a|<0　・・・・・・・・・・・・・・・・2より∧除去
4,　矛盾　・・・・・・・・・・・・・・・・・3より矛盾
5,　(a^2≦2b)　・・・・・・・・・・・・・・4の矛盾から導出
6,　(a^2≦2b)　・・・・・・・・・・・・・・1の最初の選言肢を仮定
7,　(a^2≦2b)　・・・・・・・・・・・・・・1と5と6より1の∨除去
8,　{(a^2≦2b)　∨　(2b≧0　∧　|a|<0)}→(a^2≦2b)　・・1,7より→導入
9,　(a^2≦2b)　・・・・・・・・・・・・・・仮定
10,　(a^2≦2b)　∨　(2b≧0　∧　|a|<0)　・・9より∨導入
11,　(a^2≦2b)→{(a^2≦2b)　∨　(2b≧0　∧　|a|<0)}　・・9,10より→導入
12,　(a^2≦2b)↔{(a^2≦2b)　∨　(2b≧0　∧　|a|<0)}　・・8,11より↔導入