A formalization of the first proof from [6].
© 2008 Freek Wiedijk, published by University of BiałystokThis work is licensed under the Creative Commons License.