>>942
いいけどそれ定義から帰結される定理ね