mizarは完全な証明しか受け付けない
現在の論理体系ではあのバナハ・タルスキーのパラドクスが
ＯＫとなるがいいのだろうか