比較のために、系1.8の証明(の簡略版)を掲載しておく。
―――――――――――――――――――――――――――――――――――――――――
系1.8の証明
f：R→Rであって、有理数の点で不連続, 無理数の点で微分可能となるものが存在するとする。
このとき、R−B_f は第一類集合になるので、定理1.7が適用できて、fはある開区間でリプシッツ連続である。
しかし、fは有理数の点で不連続なのだから、リプシッツ連続な開区間は取れない。よって、

「fはリプシッツ連続な開区間が取れて、fはリプシッツ連続な開区間が取れない」

となるので、矛盾する。よって、このようなfは存在しない。
―――――――――――――――――――――――――――――――――――――――――
現状での系1.8の証明とは少し違う書き方になっているが、
やっていることは同じであり、>>461と対応するように書いてみた。
両者を見比べてみるとよい。