1つの公理しか使わん定理があるんか?